Commit 2023-02-21 15:57 05d37ddf

View on Github →

feat: port LinearAlgebra.Prod (#2415)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Hom.lean

Modified Mathlib/Algebra/Module/Equiv.lean

Modified Mathlib/Algebra/Module/LinearMap.lean

Created Mathlib/LinearAlgebra/Prod.lean

added theorem LinearEquiv.coe_prod

added def LinearEquiv.prodComm

added theorem LinearEquiv.prod_apply

added theorem LinearEquiv.prod_symm

added theorem LinearEquiv.skewProd_apply

added theorem LinearEquiv.skewProd_symm_apply

added theorem LinearMap.coe_inl

added theorem LinearMap.coe_inr

added theorem LinearMap.coe_prod

added theorem LinearMap.coe_prodMap

added theorem LinearMap.comap_prod_prod

added theorem LinearMap.comp_coprod

added def LinearMap.coprod

added def LinearMap.coprodEquiv

added theorem LinearMap.coprod_apply

added theorem LinearMap.coprod_comp_prod

added theorem LinearMap.coprod_inl

added theorem LinearMap.coprod_inl_inr

added theorem LinearMap.coprod_inr

added theorem LinearMap.coprod_map_prod

added theorem LinearMap.disjoint_inl_inr

added def LinearMap.fst

added theorem LinearMap.fst_apply

added theorem LinearMap.fst_eq_coprod

added theorem LinearMap.fst_prod

added theorem LinearMap.fst_surjective

added def LinearMap.graph

added theorem LinearMap.graph_eq_ker_coprod

added theorem LinearMap.graph_eq_range_prod

added def LinearMap.inl

added theorem LinearMap.inl_apply

added theorem LinearMap.inl_eq_prod

added theorem LinearMap.inl_injective

added theorem LinearMap.inl_map_mul

added def LinearMap.inr

added theorem LinearMap.inr_apply

added theorem LinearMap.inr_eq_prod

added theorem LinearMap.inr_injective

added theorem LinearMap.inr_map_mul

added theorem LinearMap.isCompl_range_inl_inr

added theorem LinearMap.ker_coprod_of_disjoint_range

added theorem LinearMap.ker_fst

added theorem LinearMap.ker_prod

added theorem LinearMap.ker_prodMap

added theorem LinearMap.ker_prod_ker_le_ker_coprod

added theorem LinearMap.ker_snd

added theorem LinearMap.map_coprod_prod

added theorem LinearMap.mem_graph_iff

added theorem LinearMap.pair_fst_snd

added def LinearMap.prod

added def LinearMap.prodEquiv

added def LinearMap.prodMap

added def LinearMap.prodMapAlgHom

added def LinearMap.prodMapLinear

added def LinearMap.prodMapRingHom

added theorem LinearMap.prodMap_add

added theorem LinearMap.prodMap_apply

added theorem LinearMap.prodMap_comap_prod

added theorem LinearMap.prodMap_comp

added theorem LinearMap.prodMap_id

added theorem LinearMap.prodMap_mul

added theorem LinearMap.prodMap_one

added theorem LinearMap.prodMap_smul

added theorem LinearMap.prodMap_zero

added theorem LinearMap.prod_eq_inf_comap

added theorem LinearMap.prod_eq_sup_map

added theorem LinearMap.prod_ext

added theorem LinearMap.prod_ext_iff

added theorem LinearMap.range_coprod

added theorem LinearMap.range_inl

added theorem LinearMap.range_inr

added theorem LinearMap.range_prod_eq

added theorem LinearMap.range_prod_le

added def LinearMap.snd

added theorem LinearMap.snd_apply

added theorem LinearMap.snd_eq_coprod

added theorem LinearMap.snd_prod

added theorem LinearMap.snd_surjective

added theorem LinearMap.span_inl_union_inr

added theorem LinearMap.sup_range_inl_inr

added def LinearMap.tailing

added def LinearMap.tailingLinearEquiv

added theorem LinearMap.tailing_disjoint_tunnel_succ

added theorem LinearMap.tailing_le_tunnel

added theorem LinearMap.tailing_sup_tunnel_succ_le_tunnel

added def LinearMap.tailings

added theorem LinearMap.tailings_disjoint_tailing

added theorem LinearMap.tailings_disjoint_tunnel

added theorem LinearMap.tailings_succ

added theorem LinearMap.tailings_zero

added def LinearMap.tunnel'

added def LinearMap.tunnel

added def LinearMap.tunnelAux

added theorem LinearMap.tunnelAux_injective

added theorem Submodule.comap_fst

added theorem Submodule.comap_snd

added def Submodule.fst

added def Submodule.fstEquiv

added theorem Submodule.fst_inf_snd

added theorem Submodule.fst_map_fst

added theorem Submodule.fst_map_snd

added theorem Submodule.fst_sup_snd

added theorem Submodule.ker_inl

added theorem Submodule.ker_inr

added theorem Submodule.le_prod_iff

added theorem Submodule.map_inl

added theorem Submodule.map_inr

added theorem Submodule.prod_comap_inl

added theorem Submodule.prod_comap_inr

added theorem Submodule.prod_eq_bot_iff

added theorem Submodule.prod_eq_top_iff

added theorem Submodule.prod_le_iff

added theorem Submodule.prod_map_fst

added theorem Submodule.prod_map_snd

added theorem Submodule.range_fst

added theorem Submodule.range_snd

added def Submodule.snd

added def Submodule.sndEquiv

added theorem Submodule.snd_map_fst

added theorem Submodule.snd_map_snd

added theorem Submodule.sup_eq_range