Theorem LinearMap.ker_inf_smul_top_eq_smul_of_flat

Modification history

2026-04-08 16:40
Mathlib/RingTheory/Smooth/Quotient.lean
feat(RingTheory/Smooth): some lemmas about formally smooth (#35675) …
Added LinearMap.ker_inf_smul_top_eq_smul_of_flatView on Github →