Mathlib Map

Theorems · Definition · group theory

WithZero

Type u_1 → Type u_1

Add an extra element 0 to a type

Defined in
Mathlib.Algebra.Group.WithOne.Defs
Cited by
586 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

WithZero.coe · cited by 186WithZero.coeMonoidWithZeroHom.ValueGroup₀ · cited by 166MonoidWithZeroHom.ValueGr…IsDedekindDomain.HeightOneSpectrum.valuation · cited by 130HeightOneSpectrum.valuati…WithZero.exp · cited by 112WithZero.expIsDedekindDomain.HeightOneSpectrum.intValuation · cited by 53HeightOneSpectrum.intValu…WithZero.map' · cited by 45WithZero.map'WithZero.log · cited by 40WithZero.logWithZero.unzero · cited by 38WithZero.unzeroWithZero.recZeroCoe · cited by 29WithZero.recZeroCoeWithZeroMulInt.toNNReal · cited by 28WithZeroMulInt.toNNRealIsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion · cited by 25adicCompletion.toCompleti…IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap · cited by 23HeightOneSpectrum.valuati…Rat.padicValuation · cited by 18Rat.padicValuationWithZero.coe_unzero · cited by 17WithZero.coe_unzeroRatFunc.inftyValuationDef · cited by 17RatFunc.inftyValuationDefWithZeroCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by684

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 684.