Theorem ValuationSubring.isIntegral_of_mem_ringOfIntegers

Modification history

2024-08-26 11:52
Mathlib/RingTheory/Valuation/AlgebraInstances.lean
feat(RingTheory/Valuation/AlgebraInstances): add instances (#15734)
Added ValuationSubring.isIntegral_of_mem_ringOfIntegersView on Github →