ne_zero typeclass #
We create a typeclass ne_zero n which carries around the fact that (n : R) ≠ 0.
Main declarations #
ne_zero:n ≠ 0as a typeclass.
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]
@[protected, instance]
def
ne_zero.invertible
{M : Type u_3}
{x : M}
[mul_zero_one_class M]
[nontrivial M]
[invertible x] :
ne_zero x
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.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_not_dvd
(M : Type u_3)
{n p : ℕ}
[add_monoid M]
[has_one M]
[char_p M p]
(h : ¬p ∣ n) :
theorem
ne_zero.of_no_zero_smul_divisors
(R : Type u_1)
(M : Type u_3)
(n : ℕ)
[comm_ring R]
[ne_zero ↑n]
[ring M]
[nontrivial M]
[algebra R M]
[no_zero_smul_divisors R M] :