Theorem ValuationSubring.integralClosure_algebraMap_injective

Modification history

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