Commit 2023-05-31 01:08 6fa529a9

View on Github →

feat: add 3 missing defs about AlternatingMap (#4509) Forward-port leanprover-community/mathlib#19069

Estimated changes

Modified Mathlib/LinearAlgebra/Alternating.lean

added theorem AlternatingMap.coe_pi

added theorem AlternatingMap.coe_prod

added theorem AlternatingMap.coe_smulRight

added def AlternatingMap.pi

added def AlternatingMap.prod

added def AlternatingMap.smulRight

added theorem LinearMap.smulRight_eq_comp

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean