Theorem ValuationSubring.algebraMap_injective

Modification history

2024-08-26 11:52

Mathlib/RingTheory/Valuation/AlgebraInstances.lean

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

Added ValuationSubring.algebraMap_injective View on Github →