Theorem Algebra.QuasiFiniteAt.of_le

Modification history

2026-01-22 12:40

Mathlib/RingTheory/QuasiFinite/Basic.lean

feat(RingTheory): predicate for `QuasiFiniteAt` (#33718)

Added Algebra.QuasiFiniteAt.of_le View on Github →