Theorem Module.Finite.exists_comp_eq_id_of_projective

Modification history

2024-11-14 10:43
Mathlib/RingTheory/Finiteness.lean
chore(RingTheory): split Finiteness.lean into many smaller files (#18964) …
Modified Module.Finite.exists_comp_eq_id_of_projectiveView on Github →
2024-11-09 14:01
Mathlib/RingTheory/Finiteness.lean
feat(LinearAlgebra/Dual): generalize results from Free to Projective (#18686) …
Added Module.Finite.exists_comp_eq_id_of_projectiveView on Github →