Prod

📁 Source: Mathlib/LinearAlgebra/Prod.lean

Statistics

Metric	Count
Definitions `prodAssoc`, `prodComm`, `prodCongr`, `prodProdProdComm`, `prodUnique`, `skewProd`, `skewSwap`, `uniqueProd`, `coprod`, `coprodEquiv`, `fst`, `graph`, `inl`, `inr`, `kerComplementEquivRange`, `prod`, `prodEquiv`, `prodMap`, `prodMapAlgHom`, `prodMapLinear`, `prodMapRingHom`, `snd`, `fst`, `fstEquiv`, `snd`, `sndEquiv`	26
Theorems `coe_prodCongr`, `coe_prodUnique`, `coe_uniqueProd`, `fst_comp_prodAssoc`, `fst_comp_prodComm`, `prodAssoc_apply`, `prodComm_apply`, `prodCongr_apply`, `prodCongr_symm`, `prodProdProdComm_apply`, `prodProdProdComm_symm`, `prodProdProdComm_toAddEquiv`, `prodUnique_apply`, `prodUnique_symm_apply`, `skewProd_apply`, `skewProd_symm_apply`, `skewSwap_apply`, `skewSwap_symm_apply`, `snd_comp_prodAssoc`, `snd_comp_prodComm`, `symm_prodComm`, `uniqueProd_apply`, `uniqueProd_symm_apply`, `coe_fst`, `coe_inl`, `coe_inr`, `coe_prod`, `coe_prodMap`, `coe_snd`, `comap_prod_prod`, `comp_coprod`, `coprodEquiv_apply`, `coprodEquiv_symm_apply`, `coprod_apply`, `coprod_comp_inl_inr`, `coprod_comp_prod`, `coprod_inl`, `coprod_inl_inr`, `coprod_inr`, `coprod_map_prod`, `coprod_zero_left`, `coprod_zero_right`, `disjoint_inl_inr`, `exists_linearEquiv_eq_graph`, `exists_range_eq_graph`, `fst_apply`, `fst_comp_inl`, `fst_comp_inr`, `fst_eq_coprod`, `fst_prod`, `fst_surjective`, `graph_eq_ker_coprod`, `graph_eq_range_prod`, `inl_apply`, `inl_eq_prod`, `inl_injective`, `inl_map_mul`, `inr_apply`, `inr_eq_prod`, `inr_injective`, `inr_map_mul`, `isCompl_range_inl_inr`, `kerComplementEquivRange_apply_coe`, `kerComplementEquivRange_symm_apply`, `ker_coprod_of_disjoint_range`, `ker_fst`, `ker_prod`, `ker_prodMap`, `ker_prod_ker_le_ker_coprod`, `ker_snd`, `map_coprod_prod`, `mem_graph_iff`, `pair_fst_snd`, `prodEquiv_apply`, `prodEquiv_symm_apply`, `prodMapAlgHom_apply_apply`, `prodMapLinear_apply`, `prodMapRingHom_apply`, `prodMap_add`, `prodMap_apply`, `prodMap_comap_prod`, `prodMap_comp`, `prodMap_id`, `prodMap_map_prod`, `prodMap_mul`, `prodMap_one`, `prodMap_smul`, `prodMap_zero`, `prod_apply`, `prod_comp`, `prod_eq_inf_comap`, `prod_eq_sup_map`, `prod_ext`, `prod_ext_iff`, `range_coprod`, `range_inl`, `range_inr`, `range_prodMap`, `range_prod_eq`, `range_prod_le`, `snd_apply`, `snd_comp_inl`, `snd_comp_inr`, `snd_eq_coprod`, `snd_prod`, `snd_surjective`, `span_inl_union_inr`, `sup_range_inl_inr`, `comap_fst`, `comap_snd`, `exists_eq_graph`, `exists_equiv_eq_graph`, `fstEquiv_apply`, `fstEquiv_symm_apply_coe`, `fst_inf_snd`, `fst_map_fst`, `fst_map_snd`, `fst_sup_snd`, `ker_inl`, `ker_inr`, `le_prod_iff`, `map_inl`, `map_inr`, `prod_comap_inl`, `prod_comap_inr`, `prod_eq_bot_iff`, `prod_eq_top_iff`, `prod_le_iff`, `prod_map_fst`, `prod_map_snd`, `range_fst`, `range_snd`, `sndEquiv_apply`, `sndEquiv_symm_apply_coe`, `snd_map_fst`, `snd_map_snd`, `sup_eq_range`	137
Total	163

LinearEquiv

Definitions

Name	Category	Theorems
`prodAssoc` 📖	CompOp	5 math math: `AffineEquiv.linear_prodAssoc`, `snd_comp_prodAssoc`, `ContinuousLinearEquiv.prodAssoc_toLinearEquiv`, `prodAssoc_apply`, `fst_comp_prodAssoc`
`prodComm` 📖	CompOp	8 math math: `LinearPMap.inverse_graph`, `fst_comp_prodComm`, `prodComm_apply`, `Submodule.prodComm_trans_prodEquivOfIsCompl`, `snd_comp_prodComm`, `symm_prodComm`, `ContinuousLinearEquiv.prodComm_toLinearEquiv`, `AffineEquiv.linear_prodComm`
`prodCongr` 📖	CompOp	8 math math: `PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp`, `LinearIsometryEquiv.withLpProdCongr_symm_apply`, `prodCongr_symm`, `prodCongr_apply`, `AffineEquiv.linear_prodCongr`, `coe_prodCongr`, `QuadraticMap.IsometryEquiv.prod_toLinearEquiv`, `QuadraticForm.dualProdProdIsometry_invFun`
`prodProdProdComm` 📖	CompOp	4 math math: `prodProdProdComm_apply`, `ContinuousLinearEquiv.prodProdProdComm_toLinearEquiv`, `prodProdProdComm_symm`, `prodProdProdComm_toAddEquiv`
`prodUnique` 📖	CompOp	3 math math: `coe_prodUnique`, `prodUnique_symm_apply`, `prodUnique_apply`
`skewProd` 📖	CompOp	2 math math: `skewProd_symm_apply`, `skewProd_apply`
`skewSwap` 📖	CompOp	2 math math: `skewSwap_symm_apply`, `skewSwap_apply`
`uniqueProd` 📖	CompOp	3 math math: `uniqueProd_apply`, `uniqueProd_symm_apply`, `coe_uniqueProd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_prodCongr` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `prodCongr` `LinearMap.prodMap`	—	`RingHomInvPair.ids`
`coe_prodUnique` 📖	mathematical	—	`EquivLike.toEquiv` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `instEquivLike` `prodUnique` `Equiv.prodUnique`	—	`RingHomInvPair.ids`
`coe_uniqueProd` 📖	mathematical	—	`EquivLike.toEquiv` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `instEquivLike` `uniqueProd` `Equiv.uniqueProd`	—	`RingHomInvPair.ids`
`fst_comp_prodAssoc` 📖	mathematical	—	`LinearMap.comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.fst` `toLinearMap` `RingHomInvPair.ids` `prodAssoc`	—	`LinearMap.prod_ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.ext`
`fst_comp_prodComm` 📖	mathematical	—	`LinearMap.comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.fst` `toLinearMap` `RingHomInvPair.ids` `prodComm` `LinearMap.snd`	—	`LinearMap.prod_ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.ext`
`prodAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `prodAssoc` `Equiv.toFun` `AddEquiv.toEquiv` `Prod.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddEquiv.prodAssoc`	—	`RingHomInvPair.ids`
`prodComm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `prodComm`	—	`RingHomInvPair.ids`
`prodCongr_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `prodCongr`	—	`RingHomInvPair.ids`
`prodCongr_symm` 📖	mathematical	—	`symm` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `prodCongr`	—	`RingHomInvPair.ids`
`prodProdProdComm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `prodProdProdComm`	—	`RingHomInvPair.ids`
`prodProdProdComm_symm` 📖	mathematical	—	`symm` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `prodProdProdComm`	—	`RingHomInvPair.ids`
`prodProdProdComm_toAddEquiv` 📖	mathematical	—	`AddEquivClass.toAddEquiv` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `instEquivLike` `Prod.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SemilinearEquivClass.toAddEquivClass` `instSemilinearEquivClass` `prodProdProdComm` `AddEquiv.prodProdProdComm`	—	`RingHomInvPair.ids` `SemilinearEquivClass.toAddEquivClass` `instSemilinearEquivClass`
`prodUnique_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `prodUnique`	—	`RingHomInvPair.ids`
`prodUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `symm` `prodUnique` `Unique.instInhabited`	—	`RingHomInvPair.ids`
`skewProd_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `skewProd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap` `LinearMap.instFunLike`	—	`RingHomInvPair.ids`
`skewProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `symm` `skewProd` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `LinearMap` `LinearMap.instFunLike`	—	`RingHomInvPair.ids`
`skewSwap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `skewSwap` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomInvPair.ids`
`skewSwap_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `symm` `skewSwap` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomInvPair.ids`
`snd_comp_prodAssoc` 📖	mathematical	—	`LinearMap.comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.snd` `toLinearMap` `RingHomInvPair.ids` `prodAssoc` `LinearMap.prodMap` `LinearMap.id`	—	`LinearMap.prod_ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.ext`
`snd_comp_prodComm` 📖	mathematical	—	`LinearMap.comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap.snd` `toLinearMap` `RingHomInvPair.ids` `prodComm` `LinearMap.fst`	—	`LinearMap.prod_ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.ext`
`symm_prodComm` 📖	mathematical	—	`symm` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `prodComm`	—	`RingHomInvPair.ids`
`uniqueProd_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `uniqueProd`	—	`RingHomInvPair.ids`
`uniqueProd_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `instEquivLike` `symm` `uniqueProd` `Unique.instInhabited`	—	`RingHomInvPair.ids`

LinearMap

Definitions

Name	Category	Theorems
`coprod` 📖	CompOp	25 math math: `ker_coprod_of_disjoint_range`, `coprod_zero_right`, `coprod_zero_left`, `Submodule.sup_eq_range`, `Submodule.coe_prodEquivOfIsCompl`, `map_coprod_prod`, `coprod_inr`, `coprod_apply`, `ContinuousLinearMap.coe_coprod`, `trace_prodMap`, `snd_eq_coprod`, `ker_prod_ker_le_ker_coprod`, `coprod_inl_inr`, `Algebra.trace_prod`, `coprod_comp_prod`, `range_coprod`, `Module.dualProdDualEquivDual_apply`, `coprod_inl`, `coprodEquiv_apply`, `ContinuousLinearMap.ker_prod_ker_le_ker_coprod`, `coprod_map_prod`, `fst_eq_coprod`, `comp_coprod`, `coprod_comp_inl_inr`, `graph_eq_ker_coprod`
`coprodEquiv` 📖	CompOp	2 math math: `coprodEquiv_apply`, `coprodEquiv_symm_apply`
`fst` 📖	CompOp	38 math math: `prod_eq_inf_comap`, `fst_prod`, `fst_comp_inr`, `QuadraticMap.polarBilin_prod`, `fst_surjective`, `Submodule.comap_fst`, `coprod_zero_right`, `QuadraticMap.associated_prod`, `pair_fst_snd`, `LinearEquiv.fst_comp_prodComm`, `Submodule.snd_map_fst`, `coe_fst`, `prodEquiv_symm_apply`, `Function.Exact.inr_fst`, `LinearEquiv.snd_comp_prodComm`, `Submodule.toLinearPMap_domain`, `ModuleCat.binaryProductLimitCone_cone_π_app_left`, `Submodule.fst_map_fst`, `fst_apply`, `range_inr`, `dualTensorHom_prodMap_zero`, `Prod.comul_comp_fst`, `Submodule.toLinearPMap_apply_aux`, `fst_comp_inl`, `Matrix.toLin_finTwoProd`, `ModuleCat.binaryProductLimitCone_isLimit_lift`, `ker_fst`, `ModuleCat.biprodIsoProd_inv_comp_fst`, `LinearEquiv.fst_comp_prodAssoc`, `ContinuousLinearMap.coe_fst`, `fst_eq_coprod`, `AffineMap.fst_linear`, `Submodule.prod_map_fst`, `LinearPMap.graph_map_fst_eq_domain`, `Submodule.le_prod_iff`, `Algebra.Generators.CotangentSpace.fst_compEquiv`, `Submodule.mem_graph_toLinearPMap`, `Submodule.range_fst`
`graph` 📖	CompOp	9 math math: `exists_linearEquiv_eq_graph`, `Submodule.goursat`, `graph_eq_range_prod`, `Submodule.exists_eq_graph`, `mem_graph_iff`, `Submodule.goursat_surjective`, `Submodule.exists_equiv_eq_graph`, `graph_eq_ker_coprod`, `exists_range_eq_graph`
`inl` 📖	CompOp	42 math math: `inl_map_mul`, `inl_injective`, `isCompl_range_inl_inr`, `disjoint_inl_inr`, `OrthonormalBasis.prod_apply`, `Submodule.prod_le_iff`, `Submodule.ker_inl`, `span_inl_union_inr`, `snd_comp_inl`, `subset_tangentConeAt_prod_left`, `Module.Basis.prod_apply`, `Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_comp_inl`, `Function.Exact.split_tfae`, `sup_range_inl_inr`, `coprod_inl_inr`, `linearIndependent_inl_union_inr'`, `range_inl`, `Prod.comul_apply`, `inl_eq_prod`, `ker_snd`, `Polynomial.degreeLT.addLinearEquiv_symm_apply_inl`, `Algebra.adjoin_inl_union_inr_eq_prod`, `Function.Exact.split_tfae'`, `prod_ext_iff`, `coe_inl`, `LinearIndependent.inl_union_inr`, `coprod_inl`, `Submodule.map_inl`, `dualTensorHom_prodMap_zero`, `Submodule.prod_comap_inl`, `QuadraticForm.dualProdProdIsometry_toFun`, `fst_comp_inl`, `inl_apply`, `Prod.comul_comp_inl`, `Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis`, `ContinuousLinearMap.coe_inl`, `coprodEquiv_symm_apply`, `coprod_comp_inl_inr`, `Prod.counit_comp_inl`, `Function.Exact.inl_snd`, `Module.dualProdDualEquivDual_symm_apply`, `prod_eq_sup_map`
`inr` 📖	CompOp	40 math math: `Polynomial.degreeLT.addLinearEquiv_symm_apply_inr`, `inr_apply`, `fst_comp_inr`, `Prod.counit_comp_inr`, `zero_prodMap_dualTensorHom`, `coe_inr`, `Submodule.prod_comap_inr`, `isCompl_range_inl_inr`, `disjoint_inl_inr`, `OrthonormalBasis.prod_apply`, `Submodule.prod_le_iff`, `span_inl_union_inr`, `coprod_inr`, `subset_tangentConeAt_prod_right`, `Module.Basis.prod_apply`, `sup_range_inl_inr`, `ContinuousLinearMap.coe_inr`, `coprod_inl_inr`, `inr_injective`, `linearIndependent_inl_union_inr'`, `Prod.comul_apply`, `Function.Exact.inr_fst`, `Submodule.map_inr`, `Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis`, `Algebra.adjoin_inl_union_inr_eq_prod`, `prod_ext_iff`, `LinearIndependent.inl_union_inr`, `range_inr`, `Algebra.Generators.CotangentSpace.compEquiv_symm_inr`, `inr_eq_prod`, `QuadraticForm.dualProdProdIsometry_toFun`, `snd_comp_inr`, `ker_fst`, `Prod.comul_comp_inr`, `Submodule.ker_inr`, `coprodEquiv_symm_apply`, `coprod_comp_inl_inr`, `inr_map_mul`, `Module.dualProdDualEquivDual_symm_apply`, `prod_eq_sup_map`
`kerComplementEquivRange` 📖	CompOp	2 math math: `kerComplementEquivRange_apply_coe`, `kerComplementEquivRange_symm_apply`
`prod` 📖	CompOp	21 math math: `prod_comp`, `fst_prod`, `coe_equivProdOfSurjectiveOfIsCompl`, `prodEquiv_apply`, `pair_fst_snd`, `graph_eq_range_prod`, `coe_prod`, `AffineMap.prod_linear`, `range_prod_eq`, `inl_eq_prod`, `coprod_comp_prod`, `Submodule.toLinearMap_prodEquivOfIsCompl_symm`, `range_prod_le`, `snd_prod`, `inr_eq_prod`, `ker_prod`, `comap_prod_prod`, `Matrix.toLin_finTwoProd`, `ModuleCat.binaryProductLimitCone_isLimit_lift`, `prod_apply`, `ContinuousLinearMap.coe_prod`
`prodEquiv` 📖	CompOp	2 math math: `prodEquiv_apply`, `prodEquiv_symm_apply`
`prodMap` 📖	CompOp	34 math math: `range_prodMap`, `prodMap_one`, `LinearPMap.neg_graph`, `prodMap_add`, `prodMap_apply`, `zero_prodMap_dualTensorHom`, `prodMap_comap_prod`, `prodMap_comp`, `Submodule.goursat`, `IsProj.eq_conj_prodMap`, `prodMap_id`, `ker_prodMap`, `det_prodMap`, `trace_prodMap`, `prodMapLinear_apply`, `IsBaseChange.prodMap`, `LinearEquiv.snd_comp_prodAssoc`, `AffineMap.prodMap_linear`, `toMatrix_prodMap`, `IsLocalizedModule.prodMap`, `prodMap_zero`, `prodMap_map_prod`, `IsProj.eq_conj_prod_map'`, `dualTensorHom_prodMap_zero`, `coe_prodMap`, `charpoly_prodMap`, `prodMap_smul`, `LinearPMap.smul_graph`, `ContinuousLinearMap.coe_prodMap`, `trace_prodMap'`, `LinearEquiv.coe_prodCongr`, `Submodule.goursat_surjective`, `prodMap_mul`, `prodMapRingHom_apply`
`prodMapAlgHom` 📖	CompOp	1 math math: `prodMapAlgHom_apply_apply`
`prodMapLinear` 📖	CompOp	2 math math: `trace_prodMap`, `prodMapLinear_apply`
`prodMapRingHom` 📖	CompOp	1 math math: `prodMapRingHom_apply`
`snd` 📖	CompOp	38 math math: `prod_eq_inf_comap`, `Submodule.range_snd`, `QuadraticMap.polarBilin_prod`, `ContinuousLinearMap.coe_snd`, `zero_prodMap_dualTensorHom`, `Submodule.toLinearPMap_range`, `coprod_zero_left`, `QuadraticMap.associated_prod`, `pair_fst_snd`, `ModuleCat.binaryProductLimitCone_cone_π_app_right`, `snd_comp_inl`, `LinearEquiv.fst_comp_prodComm`, `prodEquiv_symm_apply`, `snd_eq_coprod`, `Submodule.snd_map_snd`, `Function.Exact.split_tfae`, `ModuleCat.biprodIsoProd_inv_comp_snd`, `Algebra.Generators.snd_comp_cotangentCompLocalizationAwayEquiv`, `range_inl`, `Submodule.comap_snd`, `ker_snd`, `LinearEquiv.snd_comp_prodComm`, `coe_snd`, `LinearEquiv.snd_comp_prodAssoc`, `Function.Exact.split_tfae'`, `Submodule.fst_map_snd`, `snd_prod`, `Prod.comul_comp_snd`, `snd_comp_inr`, `Matrix.toLin_finTwoProd`, `ModuleCat.binaryProductLimitCone_isLimit_lift`, `AffineMap.snd_linear`, `snd_surjective`, `Submodule.le_prod_iff`, `Function.Exact.inl_snd`, `LinearPMap.graph_map_snd_eq_range`, `snd_apply`, `Submodule.prod_map_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_fst` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `fst`	—	—
`coe_inl` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`coe_inr` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `inr` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`coe_prod` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `prod` `Pi.prod`	—	—
`coe_prodMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `prodMap`	—	—
`coe_snd` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `snd`	—	—
`comap_prod_prod` 📖	mathematical	—	`Submodule.comap` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `prod` `Submodule.prod` `Submodule` `Submodule.instMin`	—	`Submodule.ext`
`comp_coprod` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `coprod`	—	`ext` `RingHomCompTriple.ids` `map_add`
`coprodEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `Prod.instAddCommMonoid` `Prod.instModule` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `coprodEquiv` `coprod`	—	`RingHomInvPair.ids`
`coprodEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `Prod.instAddCommMonoid` `Prod.instModule` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `coprodEquiv` `comp` `inl` `inr`	—	`RingHomInvPair.ids`
`coprod_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `coprod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`coprod_comp_inl_inr` 📖	mathematical	—	`coprod` `comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `inl` `inr`	—	`RingHomCompTriple.ids` `comp_coprod` `coprod_inl_inr` `comp_id`
`coprod_comp_prod` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `coprod` `prod` `LinearMap` `instAdd`	—	`RingHomCompTriple.ids`
`coprod_inl` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `coprod` `inl`	—	`ext` `RingHomCompTriple.ids` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `add_zero`
`coprod_inl_inr` 📖	mathematical	—	`coprod` `Prod.instAddCommMonoid` `Prod.instModule` `inl` `inr` `id`	—	`ext` `add_zero` `zero_add`
`coprod_inr` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `coprod` `inr`	—	`ext` `RingHomCompTriple.ids` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `zero_add`
`coprod_map_prod` 📖	mathematical	—	`Submodule.map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `coprod` `Submodule.prod` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`SetLike.coe_injective` `RingHomSurjective.ids` `Set.image_congr` `Submodule.coe_sup` `Set.image2_add` `Set.image2_image_left` `Set.image2_image_right` `Set.image_prod`
`coprod_zero_left` 📖	mathematical	—	`coprod` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero` `comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `snd`	—	`zero_add`
`coprod_zero_right` 📖	mathematical	—	`coprod` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero` `comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `fst`	—	`add_zero`
`disjoint_inl_inr` 📖	mathematical	—	`Disjoint` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `inl` `inr`	—	`RingHomSurjective.ids`
`exists_linearEquiv_eq_graph` 📖	mathematical	`DFunLike.coe` `LinearMap` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike`	`range` `graph` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `exists_range_eq_graph` `RingHomCompTriple.right_ids` `AddHom.map_add'` `map_smul'`
`exists_range_eq_graph` 📖	mathematical	`DFunLike.coe` `LinearMap` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike`	`range` `graph`	—	`AddMonoidHom.instAddMonoidHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `AddMonoidHom.exists_mrange_eq_mgraph` `AddMonoidHom.map_add'` `mem_range` `Submodule.smul_mem` `Submodule.ext`
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `fst`	—	—
`fst_comp_inl` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `fst` `inl` `id`	—	`RingHomCompTriple.ids`
`fst_comp_inr` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `fst` `inr` `LinearMap` `instZero`	—	`RingHomCompTriple.ids`
`fst_eq_coprod` 📖	mathematical	—	`fst` `coprod` `id` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero`	—	`ext` `add_zero`
`fst_prod` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `fst` `prod`	—	`RingHomCompTriple.ids`
`fst_surjective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `fst`	—	—
`graph_eq_ker_coprod` 📖	mathematical	—	`graph` `AddCommGroup.toAddCommMonoid` `ker` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `coprod` `LinearMap` `instNeg` `id`	—	`Submodule.ext` `add_comm` `add_neg_eq_zero`
`graph_eq_range_prod` 📖	mathematical	—	`graph` `range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `prod` `id`	—	`Submodule.ext` `RingHomSurjective.ids`
`inl_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`inl_eq_prod` 📖	mathematical	—	`inl` `prod` `id` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero`	—	—
`inl_injective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `inl`	—	—
`inl_map_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `inl` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Prod.instMul`	—	`MulZeroClass.mul_zero`
`inr_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `inr` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`inr_eq_prod` 📖	mathematical	—	`inr` `prod` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero` `id`	—	—
`inr_injective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `inr`	—	—
`inr_map_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `inr` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Prod.instMul`	—	`MulZeroClass.mul_zero`
`isCompl_range_inl_inr` 📖	mathematical	—	`IsCompl` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `inl` `inr`	—	`RingHomSurjective.ids` `Submodule.disjoint_def` `codisjoint_iff_le_sup` `add_zero` `zero_add`
`kerComplementEquivRange_apply_coe` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `ker` `RingHom.id` `Semiring.toNonAssocSemiring`	`SetLike.instMembership` `Submodule.setLike` `range` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `kerComplementEquivRange` `LinearMap` `instFunLike`	—	`RingHomInvPair.ids` `RingHomSurjective.ids`
`kerComplementEquivRange_symm_apply` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `ker` `RingHom.id` `Semiring.toNonAssocSemiring`	`DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `SetLike.instMembership` `Submodule.setLike` `range` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `kerComplementEquivRange` `RingHomSurjective.invPair` `comp` `codRestrict` `Submodule.subtype` `LinearEquiv.ofInjective` `LinearEquiv.ofTop`	—	`RingHomInvPair.ids` `RingHomSurjective.ids`
`ker_coprod_of_disjoint_range` 📖	mathematical	`Disjoint` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderBot` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids`	`ker` `Prod.instAddCommMonoid` `Prod.instModule` `coprod` `Submodule.prod`	—	`RingHomSurjective.ids` `le_antisymm` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `sub_eq_zero` `sub_neg_eq_add` `Submodule.mem_bot` `Disjoint.eq_bot` `zero_add` `ker_prod_ker_le_ker_coprod`
`ker_fst` 📖	mathematical	—	`ker` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `fst` `range` `RingHomSurjective.ids` `inr`	—	`RingHomSurjective.ids` `range_inr`
`ker_prod` 📖	mathematical	—	`ker` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `prod` `Submodule` `Submodule.instMin`	—	`ker.eq_1` `Submodule.prod_bot` `comap_prod_prod`
`ker_prodMap` 📖	mathematical	—	`ker` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `prodMap` `Submodule.prod`	—	`prodMap_comap_prod` `Submodule.prod_bot`
`ker_prod_ker_le_ker_coprod` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.prod` `ker` `RingHom.id` `Semiring.toNonAssocSemiring` `coprod`	—	`add_zero`
`ker_snd` 📖	mathematical	—	`ker` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `snd` `range` `RingHomSurjective.ids` `inl`	—	`RingHomSurjective.ids` `range_inl`
`map_coprod_prod` 📖	mathematical	—	`Submodule.map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `coprod` `Submodule.prod` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`coprod_map_prod`
`mem_graph_iff` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `Submodule.setLike` `graph` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	—	—
`pair_fst_snd` 📖	mathematical	—	`prod` `Prod.instAddCommMonoid` `Prod.instModule` `fst` `snd` `id`	—	—
`prodEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `Prod.instAddCommMonoid` `Prod.instModule` `addCommMonoid` `module` `Prod.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `prodEquiv` `prod`	—	`RingHomInvPair.ids` `Prod.smulCommClass`
`prodEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `Prod.instAddCommMonoid` `Prod.instModule` `addCommMonoid` `module` `Prod.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `prodEquiv` `comp` `fst` `snd`	—	`RingHomInvPair.ids` `Prod.smulCommClass`
`prodMapAlgHom_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `AlgHom` `Module.End` `Prod.instSemiring` `Module.End.instSemiring` `Prod.algebra` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Prod.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Prod.isScalarTower` `AlgHom.funLike` `prodMapAlgHom`	—	`smulCommClass_self` `IsScalarTower.left` `Prod.smulCommClass` `Prod.isScalarTower`
`prodMapLinear_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `addCommMonoid` `module` `Prod.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instFunLike` `prodMapLinear` `prodMap`	—	`Prod.smulCommClass`
`prodMapRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `Prod.instNonAssocSemiring` `Module.End.instSemiring` `RingHom.instFunLike` `prodMapRingHom` `prodMap`	—	—
`prodMap_add` 📖	mathematical	—	`prodMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instAdd` `Prod.instAddCommMonoid` `Prod.instModule`	—	—
`prodMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `prodMap`	—	—
`prodMap_comap_prod` 📖	mathematical	—	`Submodule.comap` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `prodMap` `Submodule.prod`	—	`SetLike.coe_injective` `Set.preimage_prod_map_prod`
`prodMap_comp` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `prodMap`	—	`RingHomCompTriple.ids`
`prodMap_id` 📖	mathematical	—	`prodMap` `id` `Prod.instAddCommMonoid` `Prod.instModule`	—	—
`prodMap_map_prod` 📖	mathematical	—	`Submodule.map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `prodMap` `Submodule.prod`	—	`SetLike.coe_injective` `RingHomSurjective.ids` `Set.prodMap_image_prod`
`prodMap_mul` 📖	mathematical	—	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `Module.End.instMul` `prodMap`	—	—
`prodMap_one` 📖	mathematical	—	`prodMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End.instOne` `Prod.instAddCommMonoid` `Prod.instModule`	—	—
`prodMap_smul` 📖	mathematical	—	`prodMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Prod.instAddCommMonoid` `Prod.instModule` `Prod.distribSMul` `AddMonoid.toAddZeroClass` `Prod.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `Module.toDistribMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass`	—	—
`prodMap_zero` 📖	mathematical	—	`prodMap` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero` `Prod.instAddCommMonoid` `Prod.instModule`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `prod` `Pi.prod`	—	—
`prod_comp` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `prod`	—	`RingHomCompTriple.ids`
`prod_eq_inf_comap` 📖	mathematical	—	`Submodule.prod` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `Submodule.instMin` `Submodule.comap` `RingHom.id` `Semiring.toNonAssocSemiring` `fst` `snd`	—	`Submodule.ext`
`prod_eq_sup_map` 📖	mathematical	—	`Submodule.prod` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `inl` `inr`	—	`RingHomSurjective.ids` `map_coprod_prod` `coprod_inl_inr` `Submodule.map_id`
`prod_ext` 📖	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `inl` `inr`	—	—	`RingHomCompTriple.ids` `prod_ext_iff`
`prod_ext_iff` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `inl` `inr`	—	`RingHomInvPair.ids` `AddMonoid.nat_smulCommClass'` `RingHomCompTriple.ids` `LinearEquiv.injective`
`range_coprod` 📖	mathematical	—	`range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `coprod` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`Submodule.ext` `RingHomSurjective.ids`
`range_inl` 📖	mathematical	—	`range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `inl` `ker` `snd`	—	`Submodule.ext` `RingHomSurjective.ids`
`range_inr` 📖	mathematical	—	`range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `inr` `ker` `fst`	—	`Submodule.ext` `RingHomSurjective.ids`
`range_prodMap` 📖	mathematical	—	`range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `prodMap` `Submodule.prod`	—	`Submodule.ext` `RingHomSurjective.ids`
`range_prod_eq` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Top.top` `Submodule.instTop`	`range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomSurjective.ids` `prod` `Submodule.prod`	—	`le_antisymm` `RingHomSurjective.ids` `range_prod_le` `instIsConcreteLE` `sub_mem_ker_iff` `Submodule.mem_sup` `add_sub_cancel_right` `map_add` `SemilinearMapClass.toAddHomClass` `semilinearMapClass` `eq_sub_iff_add_eq` `mem_ker` `add_zero`
`range_prod_le` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `prod` `Submodule.prod`	—	`RingHomSurjective.ids` `instIsConcreteLE`
`snd_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `snd`	—	—
`snd_comp_inl` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `snd` `inl` `LinearMap` `instZero`	—	`RingHomCompTriple.ids`
`snd_comp_inr` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `snd` `inr` `id`	—	`RingHomCompTriple.ids`
`snd_eq_coprod` 📖	mathematical	—	`snd` `coprod` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instZero` `id`	—	`ext` `zero_add`
`snd_prod` 📖	mathematical	—	`comp` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `snd` `prod`	—	`RingHomCompTriple.ids`
`snd_surjective` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike` `snd`	—	—
`span_inl_union_inr` 📖	mathematical	—	`Submodule.span` `Prod.instAddCommMonoid` `Prod.instModule` `Set` `Set.instUnion` `Set.image` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `inl` `inr` `Submodule.prod`	—	`Submodule.span_union` `RingHomSurjective.ids` `prod_eq_sup_map` `Submodule.span_image`
`sup_range_inl_inr` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `inl` `inr` `Top.top` `Submodule.instTop`	—	`IsCompl.sup_eq_top` `RingHomSurjective.ids` `isCompl_range_inl_inr`

Submodule

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	6 math math: `fst_sup_snd`, `fst_inf_snd`, `fst_map_fst`, `fst_map_snd`, `fstEquiv_symm_apply_coe`, `fstEquiv_apply`
`fstEquiv` 📖	CompOp	2 math math: `fstEquiv_symm_apply_coe`, `fstEquiv_apply`
`snd` 📖	CompOp	6 math math: `fst_sup_snd`, `snd_map_fst`, `fst_inf_snd`, `snd_map_snd`, `sndEquiv_apply`, `sndEquiv_symm_apply_coe`
`sndEquiv` 📖	CompOp	2 math math: `sndEquiv_apply`, `sndEquiv_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_fst` 📖	mathematical	—	`comap` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.fst` `prod` `Top.top` `Submodule` `instTop`	—	`ext`
`comap_snd` 📖	mathematical	—	`comap` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.snd` `prod` `Top.top` `Submodule` `instTop`	—	`ext`
`exists_eq_graph` 📖	mathematical	`Function.Bijective` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `LinearMap.instFunLike` `subtype`	`LinearMap.graph`	—	`RingHomSurjective.ids` `range_subtype` `LinearMap.exists_range_eq_graph` `Function.Bijective.surjective` `Function.Bijective.injective`
`exists_equiv_eq_graph` 📖	mathematical	`Function.Bijective` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `LinearMap.instFunLike` `subtype`	`LinearMap.graph` `LinearEquiv.toLinearMap` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `RingHomSurjective.ids` `range_subtype` `LinearMap.exists_linearEquiv_eq_graph` `Function.Bijective.surjective` `Function.Bijective.injective`
`fstEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `setLike` `fst` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `fstEquiv`	—	`RingHomInvPair.ids`
`fstEquiv_symm_apply_coe` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `setLike` `fst` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `fstEquiv` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids`
`fst_inf_snd` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `instMin` `fst` `snd` `Bot.bot` `instBot`	—	`ext`
`fst_map_fst` 📖	mathematical	—	`map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst` `fst` `Top.top` `Submodule` `instTop`	—	`ext` `RingHomSurjective.ids`
`fst_map_snd` 📖	mathematical	—	`map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.snd` `fst` `Bot.bot` `Submodule` `instBot`	—	`RingHomSurjective.ids` `ext` `Zero.instNonempty`
`fst_sup_snd` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `fst` `snd` `Top.top` `instTop`	—	`eq_top_iff` `add_zero` `zero_add` `add_mem` `mem_sup_left` `mem_comap` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass` `mem_sup_right`
`ker_inl` 📖	mathematical	—	`LinearMap.ker` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.inl` `Bot.bot` `Submodule` `instBot`	—	`LinearMap.ker.eq_1` `prod_bot` `prod_comap_inl`
`ker_inr` 📖	mathematical	—	`LinearMap.ker` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.inr` `Bot.bot` `Submodule` `instBot`	—	`LinearMap.ker.eq_1` `prod_bot` `prod_comap_inr`
`le_prod_iff` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `prod` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst` `LinearMap.snd`	—	`RingHomSurjective.ids`
`map_inl` 📖	mathematical	—	`map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.inl` `prod` `Bot.bot` `Submodule` `instBot`	—	`ext` `RingHomSurjective.ids`
`map_inr` 📖	mathematical	—	`map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.inr` `prod` `Bot.bot` `Submodule` `instBot`	—	`ext` `RingHomSurjective.ids`
`prod_comap_inl` 📖	mathematical	—	`comap` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.inl` `prod`	—	`ext` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass`
`prod_comap_inr` 📖	mathematical	—	`comap` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.inr` `prod`	—	`ext` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass`
`prod_eq_bot_iff` 📖	mathematical	—	`prod` `Bot.bot` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `instBot`	—	`RingHomSurjective.ids` `GaloisConnection.le_iff_le` `gc_map_comap` `ker_inl` `ker_inr`
`prod_eq_top_iff` 📖	mathematical	—	`prod` `Top.top` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `instTop`	—	`RingHomSurjective.ids` `map_top` `range_fst` `range_snd`
`prod_le_iff` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `prod` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.inl` `LinearMap.inr`	—	`RingHomSurjective.ids` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass` `map_inl` `map_inr` `add_zero` `zero_add` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass`
`prod_map_fst` 📖	mathematical	—	`map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst` `prod`	—	`ext` `RingHomSurjective.ids` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass`
`prod_map_snd` 📖	mathematical	—	`map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.snd` `prod`	—	`ext` `RingHomSurjective.ids` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass`
`range_fst` 📖	mathematical	—	`LinearMap.range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst` `Top.top` `Submodule` `instTop`	—	`RingHomSurjective.ids` `LinearMap.range_eq_map` `prod_top` `prod_map_fst`
`range_snd` 📖	mathematical	—	`LinearMap.range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.snd` `Top.top` `Submodule` `instTop`	—	`RingHomSurjective.ids` `LinearMap.range_eq_map` `prod_top` `prod_map_snd`
`sndEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `setLike` `snd` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `sndEquiv`	—	`RingHomInvPair.ids`
`sndEquiv_symm_apply_coe` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `setLike` `snd` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `sndEquiv` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids`
`snd_map_fst` 📖	mathematical	—	`map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.fst` `snd` `Bot.bot` `Submodule` `instBot`	—	`RingHomSurjective.ids` `ext` `Zero.instNonempty`
`snd_map_snd` 📖	mathematical	—	`map` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.snd` `snd` `Top.top` `Submodule` `instTop`	—	`ext` `RingHomSurjective.ids`
`sup_eq_range` 📖	mathematical	—	`Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `LinearMap.range` `SetLike.instMembership` `setLike` `Prod.instAddCommMonoid` `addCommMonoid` `Prod.instModule` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.coprod` `subtype`	—	`ext` `RingHomSurjective.ids`

---

← Back to Index