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.

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

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

theorem pullback_nonzero {M₀ : Type u_1} {M₀' : Type u_2} [MulZeroOneClass M₀] [Nontrivial M₀] [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_3} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : a⁻¹ ≠ 0

@[simp]

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