Commit 2024-08-26 11:52 99694919

View on Github →

feat(RingTheory/Valuation/AlgebraInstances): add instances (#15734)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Valuation/AlgebraInstances.lean

added theorem ValuationSubring.algebraMap_injective

added theorem ValuationSubring.integralClosure_algebraMap_injective

added theorem ValuationSubring.isIntegral_of_mem_ringOfIntegers'

added theorem ValuationSubring.isIntegral_of_mem_ringOfIntegers