Theorem ValuationSubring.valuation_eq_one_iff

Modification history

2025-11-12 10:34
Mathlib/RingTheory/Valuation/ValuationSubring.lean
chore: rename `isUnit_of_mul_eq_one` to `IsUnit.of_mul_eq_one` (#31283) …
Modified ValuationSubring.valuation_eq_one_iffView on Github →
2023-06-21 16:11
Mathlib/RingTheory/Valuation/ValuationSubring.lean
feat: port RingTheory.Valuation.ValuationSubring (#4791)
Added ValuationSubring.valuation_eq_one_iffView on Github →