Commit 2023-01-20 15:59 a67854cc

View on Github →

feat: port Algebra.Module.LinearMap (#1587) Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/algebra.2Emodule.2Elinear_map.20mathlib4.231587

Estimated changes

added theorem IsLinearMap.map_neg
added theorem IsLinearMap.map_sub
added theorem IsLinearMap.map_zero
added def IsLinearMap.mk'
added theorem IsLinearMap.mk'_apply
added structure IsLinearMap
added theorem LinearMap.add_apply
added theorem LinearMap.add_comp
added theorem LinearMap.cancel_left
added theorem LinearMap.cancel_right
added theorem LinearMap.coe_comp
added theorem LinearMap.coe_copy
added theorem LinearMap.coe_mk
added theorem LinearMap.coe_mul
added theorem LinearMap.coe_one
added theorem LinearMap.coe_smul
added def LinearMap.comp
added theorem LinearMap.comp_add
added theorem LinearMap.comp_apply
added theorem LinearMap.comp_id
added theorem LinearMap.comp_neg
added theorem LinearMap.comp_smul
added theorem LinearMap.comp_sub
added theorem LinearMap.comp_zero
added theorem LinearMap.copy_eq
added theorem LinearMap.default_def
added theorem LinearMap.ext
added theorem LinearMap.ext_iff
added theorem LinearMap.ext_ring
added theorem LinearMap.ext_ring_iff
added theorem LinearMap.ext_ring_op
added def LinearMap.id
added theorem LinearMap.id_apply
added theorem LinearMap.id_coe
added theorem LinearMap.id_comp
added theorem LinearMap.isLinear
added theorem LinearMap.mk_coe
added theorem LinearMap.mul_apply
added theorem LinearMap.mul_eq_comp
added theorem LinearMap.neg_apply
added theorem LinearMap.neg_comp
added theorem LinearMap.one_apply
added theorem LinearMap.one_eq_id
added theorem LinearMap.smul_apply
added theorem LinearMap.smul_comp
added theorem LinearMap.sub_apply
added theorem LinearMap.sub_comp
added theorem LinearMap.zero_apply
added theorem LinearMap.zero_comp
added structure LinearMap
added theorem image_smul_set
added theorem image_smul_setₛₗ
added theorem preimage_smul_set