Theorem Valuation.toMonoidWithZeroHom_injective

Modification history

2026-06-08 12:41
Mathlib/RingTheory/Valuation/Basic.lean
chore(Data/{FunLike/SetLike}): unprime `coe_injective'` (#40215) …
Added Valuation.toMonoidWithZeroHom_injectiveView on Github →