Theorem Valuation.embedding_restrict

Modification history

2026-06-06 05:44

Mathlib/RingTheory/Valuation/Basic.lean

fix(RingTheory/Valuation): change `ValueGroup` from taking HomClass to Hom (#36911) …

Modified Valuation.embedding_restrict View on Github →

2026-03-05 11:23

Mathlib/RingTheory/Valuation/Basic.lean

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

Added Valuation.embedding_restrict View on Github →