WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Invertible matrix

Revision #3113 → #3237 · back to history

modifiedOne-sided inverse implies two-sided11eaf6802719
FieldFrom #3113To #3237
mathlib.declMatrix.mul_eq_one_commmul_eq_one_comm
provenanceaiai-moderated