Theorem Valuation.HasExtension.mk_smul_mk

Modification history

2026-01-12 13:34
Mathlib/RingTheory/Valuation/Extension.lean
feat(Algebra): more `Module.IsTorsionFree` API (#33871) …
Added Valuation.HasExtension.mk_smul_mkView on Github →