Theorem Valuation.restrict_inj

Modification history

2026-08-01 16:40

Mathlib/RingTheory/Valuation/Basic.lean

chore(RingTheory/Valuation/Basic): remove all `set_option`s in this file (#42335)

Modified Valuation.restrict_inj View on Github →

2026-03-05 11:23

Mathlib/RingTheory/Valuation/Basic.lean

feat(RingTheory/Valuation): add API (#36110) …

Added Valuation.restrict_inj View on Github →