Theorem Valuation.one_apply_of_ne_zero

Modification history

2026-08-11 00:21

Mathlib/RingTheory/Valuation/Basic.lean

chore: bump toolchain to v4.34.0-rc1 (#42619)

Modified Valuation.one_apply_of_ne_zero View on Github →

2025-08-11 11:23

Mathlib/RingTheory/Valuation/Basic.lean

feat(RingTheory/Valuation): the trivial valuation, as One (Valuation R Γ₀) (#27312)

Added Valuation.one_apply_of_ne_zero View on Github →