NeZero 1 in a nontrivial MulZeroOneClass.

This file exists to minimize the dependencies of Mathlib.Algebra.GroupWithZero.Defs, which is a part of the algebraic hierarchy used by basic tactics.

instance NeZero.one {M₀ : Type u_1} [MulZeroOneClass M₀] [Nontrivial M₀] : NeZero 1

In a nontrivial monoid with zero, zero and one are different.

Equations

• @NeZero.one = @NeZero.one.proof_1

theorem pullback_nonzero {M₀ : Type u_2} [MulZeroOneClass M₀] [Nontrivial M₀] {M₀' : Type u_1} [Zero M₀'] [One M₀'] (f : M₀' → M₀) (zero : f 0 = 0) (one : f 1 = 1) : Nontrivial M₀'

Pullback a Nontrivial instance along a function sending 0 to 0 and 1 to 1.

theorem inv_ne_zero {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : a⁻¹ ≠ 0

@[simp]

theorem inv_mul_cancel {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : a⁻¹ * a = 1