Mathlib Map

Theorems · Theorem · group theory

not_isUnit_zero

∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀], ¬IsUnit 0
Defined in
Mathlib.Algebra.GroupWithZero.Units.Basic
Cited by
20 results in Mathlib
Foundations
Depth 11 from the axioms · uses no axioms
Assumes
MonoidWithZeroNontrivial
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MulChar.map_zero · cited by 10MulChar.map_zerospectrum.nonempty · cited by 8spectrum.nonemptyminpoly.not_isUnit · cited by 4minpoly.not_isUnitnot_isCoprime_zero_zero · cited by 3not_isCoprime_zero_zeroisUnit_ringInverse · cited by 2isUnit_ringInversecard_units_lt · cited by 2card_units_ltCFC.isUnit_rpow_iff · cited by 2CFC.isUnit_rpow_iffCFC.spectrum_algebraMap_eq · cited by 2CFC.spectrum_algebraMap_eqRing.inverse_zero · cited by 2Ring.inverse_zerodivRadical_dvd_derivative · cited by 1divRadical_dvd_derivativenot_isRelPrime_zero_zero · cited by 1not_isRelPrime_zero_zeroCFC.isUnit_sqrt_iff_isStrictlyPositive · cited by 1CFC.isUnit_sqrt_iff_isStr…Cardinal.isUnit_iff · cited by 1Cardinal.isUnit_iffDirichletCharacter.modZero_eq_delta · cited by 1DirichletCharacter.modZer…MulChar.isQuadratic_iff_sq_eq_one · cited by 1MulChar.isQuadratic_iff_s…Nontrivial · cited by 2416NontrivialIsUnit · cited by 1602IsUnitMonoidWithZero · cited by 456MonoidWithZerozero_ne_one · cited by 90zero_ne_oneisUnit_zero_iff · cited by 4isUnit_zero_iffnot_isUnit_zeroCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by20

Results whose statement or proof uses this declaration.