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.
In a nontrivial monoid with zero, zero and one are different.
Equations
- ⋯ = ⋯
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
.
@[simp]