Mathlib Changelog
v4
Changelog
About
Github
Theorem
ValuationSubring.inv_mem_nonunits_iff
Modification history
2025-12-15 10:15
Mathlib/RingTheory/Valuation/ValuationSubring.lean
feat(Algebra): prerequisites for #31919 (#32118) …
Added
ValuationSubring.inv_mem_nonunits_iff
View on Github →