Theorem Algebra.WeaklyQuasiFiniteAt.eq_of_le_of_under_eq

Modification history

2026-02-13 17:17
Mathlib/RingTheory/QuasiFinite/Weakly.lean
feat(RingTheory): weakly quasi finite primes (#35234)
Added Algebra.WeaklyQuasiFiniteAt.eq_of_le_of_under_eqView on Github →