Commit 2025-08-11 11:23 f8b8b9f7

View on Github →

feat(RingTheory/Valuation): the trivial valuation, as One (Valuation R Γ₀) (#27312)

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Hom.lean

added theorem MonoidWithZeroHom.one_apply_def

added theorem MonoidWithZeroHom.one_apply_eq_zero_iff

Modified Mathlib/RingTheory/Valuation/Basic.lean

added theorem Valuation.not_isNontrivial_one

added theorem Valuation.one_apply_def

added theorem Valuation.one_apply_eq_zero_iff

added theorem Valuation.one_apply_le_one

added theorem Valuation.one_apply_lt_one_iff

added theorem Valuation.one_apply_of_ne_zero

added theorem Valuation.toMonoidWithZeroHom_one