LinearMapPiProd

📁 Source: Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

Statistics

Metric	Count
Definitions `coprod`, `coprodEquiv`, `fst`, `inl`, `inr`, `pi`, `prod`, `prodEquiv`, `prodMap`, `prodₗ`, `proj`, `single`, `snd`, `compRightL`	14
Theorems `coe_coprod`, `coe_fst`, `coe_fst'`, `coe_inl`, `coe_inr`, `coe_pi`, `coe_pi'`, `coe_prod`, `coe_prodMap`, `coe_prodMap'`, `coe_proj`, `coe_snd`, `coe_snd'`, `comp_coprod`, `comp_fst_add_comp_snd`, `comp_inl_add_comp_inr`, `coprodEquiv_apply`, `coprodEquiv_symm_apply`, `coprod_add`, `coprod_apply`, `coprod_comp_inl`, `coprod_comp_inl_inr`, `coprod_comp_inr`, `coprod_inl_inr`, `fst_comp_inl`, `fst_comp_inr`, `fst_comp_prod`, `fst_prod_snd`, `iInf_ker_proj`, `inl_apply`, `inr_apply`, `ker_coprod_of_disjoint_range`, `ker_prod`, `ker_prod_ker_le_ker_coprod`, `pi_apply`, `pi_comp`, `pi_eq_zero`, `pi_proj`, `pi_proj_comp`, `pi_zero`, `prodEquiv_apply`, `prod_apply`, `prod_ext`, `prod_ext_iff`, `prodₗ_apply`, `proj_apply`, `proj_pi`, `range_coprod`, `range_prod_eq`, `single_apply`, `snd_comp_inl`, `snd_comp_inr`, `snd_comp_prod`, `sum_comp_single`, `compRightL_apply`	55
Total	69

ContinuousLinearMap

Definitions

Name	Category	Theorems
`coprod` 📖	CompOp	18 math math: `ContinuousWithinAt.continuousLinearMapCoprod`, `coprod_comp_prodComm`, `coprodEquiv_apply`, `Submodule.coe_orthogonalDecomposition_symm`, `coe_coprod`, `coprod_comp_inl_inr`, `coprod_add`, `comp_coprod`, `Continuous.continuousLinearMapCoprod`, `ContinuousAt.continuousLinearMapCoprod`, `coprod_apply`, `coprod_comp_inr`, `coprod_comp_inl`, `ker_coprod_of_disjoint_range`, `comp_fst_add_comp_snd`, `range_coprod`, `ContinuousOn.continuousLinearMapCoprod`, `coprod_inl_inr`
`coprodEquiv` 📖	CompOp	2 math math: `coprodEquiv_apply`, `coprodEquiv_symm_apply`
`fst` 📖	CompOp	52 math math: `intervalIntegral.integral_hasFDerivAt_of_tendsto_ae`, `intervalIntegral.fderiv_integral_of_tendsto_ae`, `ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap`, `ContinuousMultilinearMap.eq_prod_iff`, `ContinuousMultilinearMap.prod_ext_iff`, `HasFDerivWithinAt.fst`, `Real.hasStrictFDerivAt_rpow_of_pos`, `norm_fst_le`, `fst_comp_prod`, `hasMFDerivAt_fst`, `Complex.hasStrictFDerivAt_cpow'`, `HasStrictFDerivAt.fst`, `mfderiv_prod_eq_add_comp`, `Complex.hasStrictFDerivAt_cpow`, `ContinuousMultilinearMap.prodEquiv_symm_apply_fst`, `hasMFDerivWithinAt_fst`, `intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae`, `Complex.hasFDerivAt_cpow`, `intervalIntegral.integral_hasStrictFDerivAt`, `ContinuousMultilinearMap.prodEquiv_symm_apply`, `hasFDerivAtFilter_fst`, `HasFDerivAtFilter.fst`, `fst_comp_inl`, `fst_comp_inr`, `hasStrictFDerivAt_fst`, `SmoothBumpCovering.comp_embeddingPiTangent_mfderiv`, `HasFDerivAt.fst`, `intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae`, `ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap`, `norm_fst`, `intervalIntegral.fderivWithin_integral_of_tendsto_ae`, `hasFDerivAt_uncurry_of_multilinear`, `hasFDerivWithinAt_fst`, `intervalIntegral.integral_hasFDerivWithinAt`, `Matrix.toLin_finTwoProd_toContinuousLinearMap`, `fderiv.fst`, `coe_fst'`, `fst_prod_snd`, `fderivWithin.fst`, `coe_fst`, `fderiv_fst`, `mfderiv_fst`, `mfderivWithin_fst`, `Real.hasStrictFDerivAt_rpow_of_neg`, `intervalIntegral.integral_hasFDerivAt`, `intervalIntegral.fderiv_integral`, `comp_fst_add_comp_snd`, `ContinuousAlternatingMap.prodLIE_symm_apply`, `HasRightInverse.fst`, `fderivWithin_fst`, `hasFDerivAt_fst`, `ContinuousMultilinearMap.hasStrictFDerivAt_uncurry`
`inl` 📖	CompOp	24 math math: `norm_inl_le_one`, `comp_inl_add_comp_inr`, `HasLeftInverse.inl`, `MeasureTheory.charFunDual_prod`, `MeasureTheory.charFunDual_eq_prod_iff`, `coprod_comp_inl_inr`, `hasFDerivAt_prodMk_left`, `prod_ext_iff`, `ProbabilityTheory.indepFun_iff_charFunDual_prod'`, `MeasureTheory.integral_continuousLinearMap_prod`, `fst_comp_inl`, `MeasureTheory.charFunDual_prod'`, `norm_inl`, `snd_comp_inl`, `inl_apply`, `ProbabilityTheory.variance_dual_prod`, `coe_inl`, `coprod_comp_inl`, `coprodEquiv_symm_apply`, `mfderiv_prod_left`, `MeasureTheory.charFunDual_eq_prod_iff'`, `coprodEquivL_symm_apply`, `coprod_inl_inr`, `ProbabilityTheory.indepFun_iff_charFunDual_prod`
`inr` 📖	CompOp	25 math math: `snd_comp_inr`, `norm_inr_le_one`, `comp_inl_add_comp_inr`, `MeasureTheory.charFunDual_prod`, `MeasureTheory.charFunDual_eq_prod_iff`, `coprod_comp_inl_inr`, `prod_ext_iff`, `coe_inr`, `norm_inr`, `ProbabilityTheory.indepFun_iff_charFunDual_prod'`, `mfderiv_prod_right`, `MeasureTheory.integral_continuousLinearMap_prod`, `inr_apply`, `IsContDiffImplicitAt.bijective`, `fst_comp_inr`, `MeasureTheory.charFunDual_prod'`, `coprod_comp_inr`, `HasLeftInverse.inr`, `ProbabilityTheory.variance_dual_prod`, `coprodEquiv_symm_apply`, `MeasureTheory.charFunDual_eq_prod_iff'`, `coprodEquivL_symm_apply`, `coprod_inl_inr`, `hasFDerivAt_prodMk_right`, `ProbabilityTheory.indepFun_iff_charFunDual_prod`
`pi` 📖	CompOp	28 math math: `hasFDerivAtFilter_pi`, `HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap`, `HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap`, `fderivWithin_pi`, `pi_apply`, `det_pi`, `pi_eq_zero`, `pi_proj`, `coe_pi`, `fderivWithin_continuousMultilinearMapCompContinuousLinearMap`, `hasFDerivAt_single`, `ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap`, `fderiv_update`, `ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM`, `hasFDerivAt_update`, `pi_comp`, `proj_pi`, `fderiv_continuousMultilinearMapCompContinuousLinearMap`, `HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap`, `norm_pi_le_of_le`, `hasFDerivWithinAt_pi`, `pi_proj_comp`, `coe_pi'`, `pi_zero`, `fderiv_pi`, `fderiv_single`, `hasStrictFDerivAt_pi`, `hasFDerivAt_pi`
`prod` 📖	CompOp	29 math math: `opNorm_prod`, `MDifferentiableAt.mfderiv_prod`, `HasMFDerivWithinAt.prodMk`, `DifferentiableAt.fderiv_prodMk`, `DifferentiableWithinAt.fderivWithin_prodMk`, `coe_equivProdOfSurjectiveOfIsCompl`, `fst_comp_prod`, `opNNNorm_prod`, `HasStrictFDerivAt.prodMk`, `HasFDerivWithinAt.inner`, `HasFDerivWithinAt.prodMk`, `Submodule.coe_orthogonalDecomposition`, `ContinuousAffineMap.prod_contLinear`, `HasFDerivAtFilter.prodMk`, `HasFDerivAt.inner`, `snd_comp_prod`, `ker_prod`, `mfderiv_prodMk`, `HasFDerivAt.prodMk`, `Matrix.toLin_finTwoProd_toContinuousLinearMap`, `prodL_apply`, `mfderivWithin_prodMk`, `prodEquiv_apply`, `fst_prod_snd`, `HasMFDerivAt.prodMk`, `range_prod_eq`, `prod_apply`, `HasStrictFDerivAt.inner`, `coe_prod`
`prodEquiv` 📖	CompOp	2 math math: `prodEquiv_apply`, `prodₗ_apply`
`prodMap` 📖	CompOp	25 math math: `HasFDerivWithinAt.prodMap`, `MDifferentiableAt.clm_prodMap`, `HasMFDerivWithinAt.prodMap`, `mfderiv_prodMap`, `MDifferentiableOn.clm_prodMap`, `HasMFDerivAt.prodMap`, `ContinuousLinearEquiv.coe_prodCongr`, `prodMapL_apply`, `ContinuousOn.prod_mapL`, `ContinuousAffineMap.prodMap_contLinear`, `MDifferentiable.clm_prodMap`, `HasLeftInverse.prodMap`, `mfderivWithin_prodMap`, `ContMDiffAt.clm_prodMap`, `ContMDiff.clm_prodMap`, `HasStrictFDerivAt.prodMap`, `HasRightInverse.prodMap`, `coe_prodMap'`, `ContMDiffWithinAt.clm_prodMap`, `coe_prodMap`, `ContMDiffOn.clm_prodMap`, `HasFDerivAt.prodMap`, `MDifferentiableWithinAt.clm_prodMap`, `Continuous.prod_mapL`, `Trivialization.coordChangeL_prod`
`prodₗ` 📖	CompOp	1 math math: `prodₗ_apply`
`proj` 📖	CompOp	37 math math: `hasStrictFDerivAt_apply`, `hasStrictFDerivAt_list_prod_finRange'`, `hasFDerivAt_multiset_prod`, `ContinuousMultilinearMap.piLinearEquiv_symm_apply`, `hasStrictFDerivAt_pi'`, `hasFDerivWithinAt_pi'`, `hasStrictFDerivAt_multiset_prod`, `det_pi`, `iInf_ker_proj`, `hasFDerivAt_finCons`, `hasFDerivWithinAt_finCons`, `proj_apply`, `pi_proj`, `ContinuousAlternatingMap.piEquiv_symm_apply`, `hasFDerivAt_apply`, `hasFTaylorSeriesUpToOn_pi'`, `hasFDerivAt_list_prod'`, `hasStrictFDerivAt_finCons`, `hasFDerivAt_list_prod_finRange'`, `hasStrictFDerivAt_list_prod_attach'`, `ContinuousAlternatingMap.piLinearEquiv_symm_apply`, `hasStrictFDerivAt_finset_prod`, `hasFDerivAtFilter_finCons`, `proj_pi`, `ContinuousMultilinearMap.piₗᵢ_symm_apply`, `SmoothBumpCovering.comp_embeddingPiTangent_mfderiv`, `hasFDerivAt_uncurry_of_multilinear`, `coe_proj`, `ContinuousMultilinearMap.piEquiv_symm_apply`, `hasStrictFDerivAt_list_prod`, `pi_proj_comp`, `hasStrictFDerivAt_list_prod'`, `hasFDerivAtFilter_pi'`, `hasFDerivAt_pi'`, `hasFDerivAt_list_prod_attach'`, `hasFDerivWithinAt_apply`, `hasFDerivAt_finset_prod`
`single` 📖	CompOp	10 math math: `sum_comp_single`, `single_apply`, `MeasureTheory.charFunDual_pi'`, `ProbabilityTheory.iIndepFun_iff_charFunDual_pi`, `norm_single`, `MeasureTheory.charFunDual_eq_pi_iff`, `ProbabilityTheory.iIndepFun_iff_charFunDual_pi'`, `MeasureTheory.charFunDual_eq_pi_iff'`, `norm_single_le_one`, `MeasureTheory.charFunDual_pi`
`snd` 📖	CompOp	51 math math: `fderiv_snd`, `snd_comp_inr`, `intervalIntegral.integral_hasFDerivAt_of_tendsto_ae`, `intervalIntegral.fderiv_integral_of_tendsto_ae`, `ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap`, `ContinuousMultilinearMap.eq_prod_iff`, `hasStrictFDerivAt_snd`, `coe_snd`, `ContinuousMultilinearMap.prod_ext_iff`, `Real.hasStrictFDerivAt_rpow_of_pos`, `hasFDerivAt_snd`, `Complex.hasStrictFDerivAt_cpow'`, `mfderiv_prod_eq_add_comp`, `Complex.hasStrictFDerivAt_cpow`, `fderivWithin.snd`, `intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae`, `Complex.hasFDerivAt_cpow`, `intervalIntegral.integral_hasStrictFDerivAt`, `fderiv.snd`, `ContinuousMultilinearMap.prodEquiv_symm_apply`, `fderivWithin_snd`, `hasFDerivAtFilter_snd`, `ContinuousMultilinearMap.prodEquiv_symm_apply_snd`, `HasFDerivWithinAt.snd`, `snd_comp_prod`, `HasFDerivAt.snd`, `mfderiv_snd`, `HasFDerivAtFilter.snd`, `intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae`, `ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap`, `hasMFDerivWithinAt_snd`, `intervalIntegral.fderivWithin_integral_of_tendsto_ae`, `hasFDerivAt_uncurry_of_multilinear`, `intervalIntegral.integral_hasFDerivWithinAt`, `Matrix.toLin_finTwoProd_toContinuousLinearMap`, `coe_snd'`, `snd_comp_inl`, `fst_prod_snd`, `HasRightInverse.snd`, `hasMFDerivAt_snd`, `norm_snd_le`, `norm_snd`, `Real.hasStrictFDerivAt_rpow_of_neg`, `intervalIntegral.integral_hasFDerivAt`, `intervalIntegral.fderiv_integral`, `comp_fst_add_comp_snd`, `ContinuousAlternatingMap.prodLIE_symm_apply`, `ContinuousMultilinearMap.hasStrictFDerivAt_uncurry`, `mfderivWithin_snd`, `hasFDerivWithinAt_snd`, `HasStrictFDerivAt.snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_coprod` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `coprod` `LinearMap.coprod`	—	—
`coe_fst` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `fst` `LinearMap.fst`	—	—
`coe_fst'` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `funLike` `fst`	—	—
`coe_inl` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `inl` `LinearMap.inl`	—	—
`coe_inr` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `inr` `LinearMap.inr`	—	—
`coe_pi` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `pi` `LinearMap.pi`	—	—
`coe_pi'` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `funLike` `pi`	—	—
`coe_prod` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `prod` `LinearMap.prod`	—	—
`coe_prodMap` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `prodMap` `LinearMap.prodMap`	—	—
`coe_prodMap'` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `funLike` `prodMap`	—	—
`coe_proj` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `proj` `LinearMap.proj`	—	—
`coe_snd` 📖	mathematical	—	`toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `snd` `LinearMap.snd`	—	—
`coe_snd'` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `funLike` `snd`	—	—
`comp_coprod` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `coprod`	—	`coe_injective` `RingHomCompTriple.ids` `LinearMap.comp_coprod`
`comp_fst_add_comp_snd` 📖	mathematical	—	`ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `add` `comp` `RingHomCompTriple.ids` `fst` `snd` `coprod`	—	`RingHomCompTriple.ids`
`comp_inl_add_comp_inr` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `funLike` `comp` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `inl` `inr`	—	`RingHomCompTriple.ids` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass` `add_zero` `zero_add`
`coprodEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousLinearMap` `instTopologicalSpaceProd` `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` `ContinuousLinearMap` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `coprodEquiv` `comp` `inl` `inr`	—	`RingHomInvPair.ids`
`coprod_add` 📖	mathematical	—	`coprod` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `add` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule`	—	`prod_ext` `ext` `RingHomCompTriple.ids` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass` `add_zero` `add_comp` `zero_add`
`coprod_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `funLike` `coprod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`coprod_comp_inl` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `coprod` `inl`	—	`coe_injective` `RingHomCompTriple.ids` `LinearMap.coprod_inl`
`coprod_comp_inl_inr` 📖	mathematical	—	`coprod` `comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `inl` `inr`	—	`RingHomCompTriple.ids` `Prod.continuousAdd` `comp_coprod` `coprod_inl_inr` `comp_id`
`coprod_comp_inr` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `coprod` `inr`	—	`coe_injective` `RingHomCompTriple.ids` `LinearMap.coprod_inr`
`coprod_inl_inr` 📖	mathematical	—	`coprod` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `Prod.continuousAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `inl` `inr` `id`	—	`coe_injective` `Prod.continuousAdd` `LinearMap.coprod_inl_inr`
`fst_comp_inl` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `fst` `inl` `id`	—	`RingHomCompTriple.ids`
`fst_comp_inr` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `fst` `inr` `ContinuousLinearMap` `zero`	—	`RingHomCompTriple.ids`
`fst_comp_prod` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `fst` `prod`	—	`ext` `RingHomCompTriple.ids`
`fst_prod_snd` 📖	mathematical	—	`prod` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `fst` `snd` `id`	—	`ext`
`iInf_ker_proj` 📖	mathematical	—	`iInf` `Submodule` `Pi.addCommMonoid` `Pi.module` `Submodule.instInfSet` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap` `Pi.topologicalSpace` `proj` `Bot.bot` `Submodule.instBot`	—	`LinearMap.iInf_ker_proj`
`inl_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `funLike` `inl` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`inr_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `funLike` `inr` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`ker_coprod_of_disjoint_range` 📖	mathematical	`Disjoint` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderBot` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `toLinearMap`	`LinearMap.ker` `Prod.instAddCommMonoid` `Prod.instModule` `instTopologicalSpaceProd` `coprod` `Submodule.prod`	—	`RingHomSurjective.ids` `LinearMap.ker_coprod_of_disjoint_range`
`ker_prod` 📖	mathematical	—	`LinearMap.ker` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap` `instTopologicalSpaceProd` `prod` `Submodule` `Submodule.instMin`	—	`LinearMap.ker_prod`
`ker_prod_ker_le_ker_coprod` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.prod` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap` `LinearMap.coprod`	—	`LinearMap.ker_prod_ker_le_ker_coprod`
`pi_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `funLike` `pi`	—	—
`pi_comp` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `RingHomCompTriple.ids` `pi`	—	`RingHomCompTriple.ids`
`pi_eq_zero` 📖	mathematical	—	`pi` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `zero`	—	`forall_swap`
`pi_proj` 📖	mathematical	—	`pi` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `proj` `id`	—	—
`pi_proj_comp` 📖	mathematical	—	`pi` `comp` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `RingHomCompTriple.ids` `proj`	—	`RingHomCompTriple.ids`
`pi_zero` 📖	mathematical	—	`pi` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `zero` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module`	—	`ext`
`prodEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodEquiv` `prod`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `funLike` `prod`	—	—
`prod_ext` 📖	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `inl` `inr`	—	—	`RingHomCompTriple.ids` `prod_ext_iff`
`prod_ext_iff` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `inl` `inr`	—	`RingHomCompTriple.ids`
`prodₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousLinearMap` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `addCommMonoid` `Prod.continuousAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `module` `Prod.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `Module.toDistribMulAction` `Prod.continuousConstSMul` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `prodₗ` `Equiv.toFun` `prodEquiv`	—	`RingHomInvPair.ids` `Prod.continuousAdd` `Prod.smulCommClass` `Prod.continuousConstSMul`
`proj_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `funLike` `proj`	—	—
`proj_pi` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `RingHomCompTriple.ids` `proj` `pi`	—	`RingHomCompTriple.ids`
`range_coprod` 📖	mathematical	—	`LinearMap.range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `toLinearMap` `instTopologicalSpaceProd` `coprod` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`LinearMap.range_coprod`
`range_prod_eq` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `toLinearMap` `Top.top` `Submodule.instTop`	`LinearMap.range` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomSurjective.ids` `instTopologicalSpaceProd` `prod` `Submodule.prod`	—	`LinearMap.range_prod_eq`
`single_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `funLike` `single` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`snd_comp_inl` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `snd` `inl` `ContinuousLinearMap` `zero`	—	`RingHomCompTriple.ids`
`snd_comp_inr` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `snd` `inr` `id`	—	`RingHomCompTriple.ids`
`snd_comp_prod` 📖	mathematical	—	`comp` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `snd` `prod`	—	`ext` `RingHomCompTriple.ids`
`sum_comp_single` 📖	mathematical	—	`Finset.sum` `Finset.univ` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `funLike` `comp` `Pi.topologicalSpace` `Pi.addCommMonoid` `Pi.module` `RingHomCompTriple.ids` `single`	—	`RingHomCompTriple.ids` `Finset.sum_congr` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass` `LinearMap.sum_single_apply`

Pi

Definitions

Name	Category	Theorems
`compRightL` 📖	CompOp	5 math math: `compRightL_apply`, `hasFDerivAt_finCons`, `hasFDerivWithinAt_finCons`, `hasStrictFDerivAt_finCons`, `hasFDerivAtFilter_finCons`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compRightL_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `topologicalSpace` `addCommMonoid` `module` `ContinuousLinearMap.funLike` `compRightL`	—	—

---

← Back to Index