ne_zero
typeclass #
We create a typeclass ne_zero n
which carries around the fact that (n : R) ≠ 0
.
Main declarations #
ne_zero
:n ≠ 0
as a typeclass.
@[protected, instance]
theorem
ne_zero.of_gt
{M : Type u_3}
{x y : M}
[canonically_ordered_add_monoid M]
(h : x < y) :
ne_zero y
@[protected, instance]
def
ne_zero.of_gt'
{M : Type u_3}
{y : M}
[canonically_ordered_add_monoid M]
[has_one M]
[fact (1 < y)] :
ne_zero y
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
ne_zero.pow
{M : Type u_3}
{x : M}
{n : ℕ}
[monoid_with_zero M]
[no_zero_divisors M]
[ne_zero x] :
@[protected, instance]
def
ne_zero.mul
{M : Type u_3}
{x y : M}
[has_zero M]
[has_mul M]
[no_zero_divisors M]
[ne_zero x]
[ne_zero y] :
@[protected, instance]
theorem
ne_zero.of_map
{R : Type u_1}
{M : Type u_3}
{F : Type u_4}
{r : R}
[has_zero R]
[has_zero M]
[zero_hom_class F R M]
(f : F)
[ne_zero (⇑f r)] :
ne_zero r
theorem
ne_zero.nat_of_ne_zero
{R : Type u_1}
{S : Type u_2}
{F : Type u_4}
{n : ℕ}
[semiring R]
[semiring S]
[ring_hom_class F R S]
(f : F)
[hn : ne_zero ↑n] :
theorem
ne_zero.of_injective
{R : Type u_1}
{M : Type u_3}
{F : Type u_4}
{r : R}
[has_zero R]
[h : ne_zero r]
[has_zero M]
[zero_hom_class F R M]
{f : F}
(hf : function.injective ⇑f) :
theorem
ne_zero.nat_of_injective
{R : Type u_1}
{M : Type u_3}
{F : Type u_4}
{n : ℕ}
[non_assoc_semiring M]
[non_assoc_semiring R]
[h : ne_zero ↑n]
[ring_hom_class F R M]
{f : F}
(hf : function.injective ⇑f) :
theorem
ne_zero.of_ne_zero_coe
(R : Type u_1)
{n : ℕ}
[add_monoid_with_one R]
[h : ne_zero ↑n] :
ne_zero n
theorem
ne_zero.pos_of_ne_zero_coe
(R : Type u_1)
{n : ℕ}
[add_monoid_with_one R]
[ne_zero ↑n] :
0 < n