WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — General linear group

Revision #1255 → #2579 · back to history

modifiedSymplectic group96c170b54424
FieldFrom #1255To #2579
mathlib.declsymplecticGroupMatrix.symplecticGroup
provenanceaiai-moderated