Theorem ValuationSubring.isIntegral_of_mem_ringOfIntegers'

Modification history

2025-12-15 10:15
Mathlib/RingTheory/Valuation/AlgebraInstances.lean
feat(Algebra): prerequisites for #31919 (#32118) …
Modified ValuationSubring.isIntegral_of_mem_ringOfIntegers'View on Github →
2024-08-26 11:52
Mathlib/RingTheory/Valuation/AlgebraInstances.lean
feat(RingTheory/Valuation/AlgebraInstances): add instances (#15734)
Added ValuationSubring.isIntegral_of_mem_ringOfIntegers'View on Github →