WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Rank–nullity theorem

Revision #2419 → #2637 · back to history

modifiedExtension of kernel basis to full basisef73fdd988ee
FieldFrom #2419To #2637
mathlib.declBasis.extendModule.Basis.extend
provenanceaiai-moderated