Theorem Valuation.map_apply

Modification history

2026-09-16 13:44

Mathlib/RingTheory/Valuation/Basic.lean

fix(Algebra/MonoidWithZeroHom): normalize to `.toMonoidWithZeroHom` (#43728) …

Modified Valuation.map_apply View on Github →

2024-11-09 15:13

Mathlib/RingTheory/Valuation/Basic.lean

feat(RingTheory/Valuation/Basic): add `map_apply` lemmas (#18781)

Added Valuation.map_apply View on Github →