Commit 2023-02-13 06:07 22222159

View on Github →

feat: port LinearAlgebra.Basic (#1979)

Estimated changes

added theorem Finsupp.smul_sum
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 theorem LinearEquiv.ker_comp
added theorem LinearEquiv.map_neg
added theorem LinearEquiv.map_sub
added theorem LinearEquiv.map_sum
added def LinearEquiv.neg
added theorem LinearEquiv.neg_apply
added def LinearEquiv.ofEq
added theorem LinearEquiv.ofEq_rfl
added theorem LinearEquiv.ofEq_symm
added theorem LinearEquiv.range_comp
added theorem LinearEquiv.symm_neg
added theorem LinearEquiv.zero_apply
added theorem LinearEquiv.zero_symm
added theorem LinearMap.coeFn_sum
added theorem LinearMap.coe_pow
added theorem LinearMap.comp_assoc
added theorem LinearMap.disjoint_ker
added theorem LinearMap.eqLocus_same
added theorem LinearMap.funLeft_comp
added theorem LinearMap.funLeft_id
added theorem LinearMap.id_pow
added theorem LinearMap.iterate_succ
added def LinearMap.ker
added theorem LinearMap.ker_comp
added theorem LinearMap.ker_eq_bot'
added theorem LinearMap.ker_eq_bot
added theorem LinearMap.ker_eq_top
added theorem LinearMap.ker_id
added theorem LinearMap.ker_le_iff
added theorem LinearMap.ker_restrict
added theorem LinearMap.ker_smul'
added theorem LinearMap.ker_smul
added theorem LinearMap.ker_zero
added theorem LinearMap.map_coe_ker
added theorem LinearMap.map_le_range
added theorem LinearMap.map_sum
added theorem LinearMap.mem_eqLocus
added theorem LinearMap.mem_ker
added theorem LinearMap.mem_range
added theorem LinearMap.pow_apply
added theorem LinearMap.pow_restrict
added def LinearMap.range
added theorem LinearMap.range_coe
added theorem LinearMap.range_comp
added theorem LinearMap.range_eq_bot
added theorem LinearMap.range_eq_map
added theorem LinearMap.range_eq_top
added theorem LinearMap.range_id
added theorem LinearMap.range_neg
added theorem LinearMap.range_smul'
added theorem LinearMap.range_smul
added theorem LinearMap.range_zero
added theorem LinearMap.sum_apply
added theorem Submodule.coe_ofLe
added def Submodule.comap
added theorem Submodule.comap_bot
added theorem Submodule.comap_coe
added theorem Submodule.comap_comp
added theorem Submodule.comap_id
added theorem Submodule.comap_inf
added theorem Submodule.comap_infᵢ
added theorem Submodule.comap_mono
added theorem Submodule.comap_smul'
added theorem Submodule.comap_smul
added theorem Submodule.comap_top
added theorem Submodule.comap_zero
added theorem Submodule.gc_map_comap
added theorem Submodule.ker_ofLe
added theorem Submodule.ker_subtype
added theorem Submodule.le_comap_map
added def Submodule.map
added theorem Submodule.map_add_le
added theorem Submodule.map_bot
added theorem Submodule.map_coe
added theorem Submodule.map_comap_eq
added theorem Submodule.map_comap_le
added theorem Submodule.map_comp
added theorem Submodule.map_id
added theorem Submodule.map_mono
added theorem Submodule.map_smul'
added theorem Submodule.map_smul
added theorem Submodule.map_sup
added theorem Submodule.map_supᵢ
added theorem Submodule.map_top
added theorem Submodule.map_zero
added theorem Submodule.mem_comap
added theorem Submodule.mem_map
added theorem Submodule.neg_coe
added def Submodule.ofLe
added theorem Submodule.ofLe_apply
added theorem Submodule.range_ofLe
added theorem pi_eq_sum_univ