Theorem Algebra.FiniteType.of_span_eq_top_source

Modification history

2026-03-03 14:56

Mathlib/RingTheory/Finiteness/FiniteTypeLocal.lean

chore(RingTheory): reorganize imports around locality properties of finiteness (#36044)

Modified Algebra.FiniteType.of_span_eq_top_source View on Github →

2025-06-28 11:35

Mathlib/RingTheory/RingHom/FiniteType.lean

refactor(RingTheory/RingHom): factor out proofs for `Algebra.FiniteType` (#22931) …

Added Algebra.FiniteType.of_span_eq_top_source View on Github →