WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Determinant

Revision #1148 → #1722 · back to history

modifiedSign of determinant gives basis orientation7a2ed7260344
FieldFrom #1148To #1722
mathlib.declBasis.orientation_eq_iff_det_posModule.Basis.orientation_eq_iff_det_pos
note`orientation_eq_iff_det_pos` characterizes equality of orientations via positivity of the change-of-basis determinant.`Module.Basis.orientation_eq_iff_det_pos` characterizes equality of orientations via positivity of the change-of-basis determinant.
addedGeneral linear group10ed5e25ba4f
addedSpecial linear group4c3e534795eb
addedDeterminant respects ring homomorphisms (naturality)cea6fa2c806c
addedCayley–Hamilton theoremaf60cb675639