Commit 2025-01-15 22:33 79a5bf8f

View on Github →

chore: split file LinearAlgebra.PerfectPairing (#20780) In preparation for some new material about restrictions of perfect pairings, it is useful first to split this file.

Estimated changes

added def LinearEquiv.flip
added theorem LinearEquiv.flip_apply
added theorem LinearEquiv.flip_flip
added theorem LinearEquiv.symm_flip
added structure PerfectPairing
deleted def LinearEquiv.flip
deleted theorem LinearEquiv.flip_apply
deleted theorem LinearEquiv.flip_flip
deleted theorem LinearEquiv.symm_flip
deleted def PerfectPairing.dual
deleted theorem PerfectPairing.finrank_eq
deleted theorem PerfectPairing.flip_flip
deleted structure PerfectPairing