Theorems · Definition · group theory
WithZero.log
{M : Type u_4} → [AddMonoid M] → WithZero (Multiplicative M) → MThe logarithm as a function Mᵐ⁰ → M with junk value log 0 = 0.
- Defined in
- Mathlib.Algebra.GroupWithZero.WithZero
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses Quot.sound
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- AddMonoidstatement and proof · cited by 2,864
- Multiplicativestatement and proof · cited by 875
- WithZerostatement and proof · cited by 586
- Multiplicative.toAddproof · cited by 161
- WithZero.recZeroCoeproof · cited by 29
Cited by40
Results whose statement or proof uses this declaration.
- WithZero.exp_logstatement and proof · cited by 8
- WithZero.log_lt_logstatement · cited by 5
- IsDedekindDomain.HeightOneSpectrum.valuation_surjectiveproof · cited by 4
- WithZero.log_onestatement · cited by 4
- WithZero.toAdd_unzero_eq_logstatement · cited by 4
- WithZero.le_log_iff_exp_lestatement and proof · cited by 3
- WithZero.log_expstatement · cited by 3
- WithZero.log_invstatement and proof · cited by 3
- WithZero.log_le_logstatement · cited by 3
- WithZero.log_mulstatement and proof · cited by 3
- WithZero.lt_log_iff_exp_ltstatement and proof · cited by 3
- IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iffproof · cited by 2