Commit 2024-03-16 19:33 bad9e36c
View on Github →feat: add Basis.flag_le_ker_dual (#11265) From sphere-eversion; I adapted the proof to mathlib's definition and golfed it a bit. This adds a new import; as this file is not imported anywhere, this seems fine.