Theorem Valuation.transcendental_of_ne_one

Modification history

2026-04-28 15:17
Mathlib/RingTheory/Valuation/IsTrivialOn.lean
feat(Valuation/IsTrivialOn): transcendental_of_lt_one (#37512) …
Added Valuation.transcendental_of_ne_oneView on Github →