Commit 2024-06-09 19:41 04c29e25

View on Github →

chore: move basic linear equivalences to Mathlib.Algebra.Module.Equiv (#13662) This means Mathlib.Algebra.Module.Equiv is starting to get a little on the large side, but I don't have a great alternative.

Estimated changes

added theorem LinearEquiv.coe_curry
added theorem LinearEquiv.coe_neg
added theorem LinearEquiv.coe_zero
added def LinearEquiv.conj
added theorem LinearEquiv.conj_apply
added theorem LinearEquiv.conj_comp
added theorem LinearEquiv.conj_id
added theorem LinearEquiv.conj_trans
added def LinearEquiv.neg
added theorem LinearEquiv.neg_apply
added theorem LinearEquiv.symm_neg
added theorem LinearEquiv.zero_apply
added theorem LinearEquiv.zero_symm
added theorem LinearMap.funLeft_comp
added theorem LinearMap.funLeft_id
deleted def Equiv.toLinearEquiv
deleted theorem LinearEquiv.coe_curry
deleted theorem LinearEquiv.coe_neg
deleted theorem LinearEquiv.coe_zero
deleted def LinearEquiv.conj
deleted theorem LinearEquiv.conj_apply
deleted theorem LinearEquiv.conj_comp
deleted theorem LinearEquiv.conj_id
deleted theorem LinearEquiv.conj_trans
deleted def LinearEquiv.neg
deleted theorem LinearEquiv.neg_apply
deleted theorem LinearEquiv.symm_neg
deleted theorem LinearEquiv.zero_apply
deleted theorem LinearEquiv.zero_symm
deleted def LinearMap.funLeft
deleted theorem LinearMap.funLeft_apply
deleted theorem LinearMap.funLeft_comp
deleted theorem LinearMap.funLeft_id