Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-14 10:50 b48cf171

View on Github →

feat(linear_algebra/alternating): Add dom_coprod (#5269) This implements a variant of the multiplication defined in the second half of Proposition 22.24 of "Notes on Differential Geometry and Lie Groups" (Jean Gallier):

Estimated changes

Modified docs/references.bib

Modified src/linear_algebra/alternating.lean

added theorem alternating_map.coe_multilinear_map_injective

added def alternating_map.dom_coprod'

added theorem alternating_map.dom_coprod'_apply

added def alternating_map.dom_coprod.summand

added theorem alternating_map.dom_coprod.summand_add_swap_smul_eq_zero

added theorem alternating_map.dom_coprod.summand_eq_zero_of_smul_invariant

added theorem alternating_map.dom_coprod.summand_mk'

added def alternating_map.dom_coprod

added theorem alternating_map.dom_coprod_coe

added theorem equiv.perm.mod_sum_congr.swap_smul_involutive

added def equiv.perm.mod_sum_congr

added theorem multilinear_map.dom_coprod_alternization

added theorem multilinear_map.dom_coprod_alternization_coe

added theorem multilinear_map.dom_coprod_alternization_eq