Pi

📁 Source: Mathlib/LinearAlgebra/Pi.lean

Statistics

Metric	Count
Definitions consLinearEquiv, linearMap, finTwoArrow, funUnique, piCongrLeft, piCongrLeft', piCongrRight, piCurry, piFinTwo, piOptionEquivProd, piRing, sumArrowLequivProdArrow, compLeft, const, diag, iInfKerProjEquiv, lsum, pi, proj, single, vecCons, vecCons₂, vecEmpty, vecEmpty₂, pi	25
Theorems consLinearEquiv_apply, consLinearEquiv_symm_apply, linearMap_apply, finTwoArrow_apply, finTwoArrow_symm_apply, funUnique_apply, funUnique_symm_apply, piCongrLeft'_apply, piCongrLeft'_symm_apply, piCongrRight_apply, piCongrRight_refl, piCongrRight_symm, piCongrRight_trans, piCurry_apply, piCurry_symm_apply, piFinTwo_apply, piFinTwo_symm_apply, piRing_apply, piRing_symm_apply, sumArrowLequivProdArrow_apply_fst, sumArrowLequivProdArrow_apply_snd, sumArrowLequivProdArrow_symm_apply_inl, sumArrowLequivProdArrow_symm_apply_inr, pi, apply_single, coe_proj, coe_single, compLeft_apply, const_apply, disjoint_single_single, iInf_ker_proj, iInf_ker_proj_le_iSup_range_single, iSup_range_single, iSup_range_single_eq_iInf_ker_proj, iSup_range_single_le_iInf_ker_proj, ker_compLeft, ker_pi, ker_single, lsum_apply, lsum_piSingle, lsum_single, lsum_symm_apply, pi_apply, pi_apply_eq_sum_univ, pi_comp, pi_eq_zero, pi_ext, pi_ext', pi_ext'_iff, pi_ext_iff, pi_proj, pi_proj_comp, pi_zero, proj_apply, proj_comp_single, proj_comp_single_ne, proj_comp_single_same, proj_pi, proj_surjective, range_compLeft, single_apply, single_eq_pi_diag, sum_single_apply, toAddMonoidHom_proj, update_apply, vecCons_apply, vecCons₂_apply, vecEmpty_apply, vecEmpty₂_apply, pi_induction, pi_induction', mem_span_range_single_inl_iff, biInf_comap_proj, coe_pi, iInf_comap_proj, iSup_map_single, iSup_map_single_le, le_comap_single_pi, mem_pi, pi_empty, pi_mono, pi_top, pi_univ_bot	83
Total	108

Fin

Definitions

Name	Category	Theorems
consLinearEquiv 📖	CompOp	2 math math: consLinearEquiv_symm_apply, consLinearEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
consLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.instAddCommMonoid Pi.addCommMonoid Prod.instModule Pi.module EquivLike.toFunLike LinearEquiv.instEquivLike consLinearEquiv Equiv.toFun consEquiv	—	RingHomInvPair.ids
consLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Prod.instAddCommMonoid Pi.module Prod.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm consLinearEquiv Equiv.invFun consEquiv	—	RingHomInvPair.ids

Function.ExtendByZero

Definitions

Name	Category	Theorems
linearMap 📖	CompOp	1 math math: linearMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike linearMap Function.extend Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—

LinearEquiv

Definitions

Name	Category	Theorems
finTwoArrow 📖	CompOp	2 math math: finTwoArrow_apply, finTwoArrow_symm_apply
funUnique 📖	CompOp	2 math math: funUnique_symm_apply, funUnique_apply
piCongrLeft 📖	CompOp	—
piCongrLeft' 📖	CompOp	2 math math: piCongrLeft'_symm_apply, piCongrLeft'_apply
piCongrRight 📖	CompOp	6 math math: piCongrRight_apply, piCongrRight_trans, MultilinearMap.freeDFinsuppEquiv_def, piCongrRight_symm, piCongrRight_refl, QuadraticMap.IsometryEquiv.pi_toLinearEquiv
piCurry 📖	CompOp	2 math math: piCurry_apply, piCurry_symm_apply
piFinTwo 📖	CompOp	2 math math: piFinTwo_symm_apply, piFinTwo_apply
piOptionEquivProd 📖	CompOp	—
piRing 📖	CompOp	2 math math: piRing_symm_apply, piRing_apply
sumArrowLequivProdArrow 📖	CompOp	4 math math: sumArrowLequivProdArrow_symm_apply_inr, sumArrowLequivProdArrow_apply_fst, sumArrowLequivProdArrow_apply_snd, sumArrowLequivProdArrow_symm_apply_inl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finTwoArrow_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Prod.instAddCommMonoid Pi.Function.module Prod.instModule EquivLike.toFunLike instEquivLike finTwoArrow	—	RingHomInvPair.ids
finTwoArrow_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.instAddCommMonoid Pi.addCommMonoid Prod.instModule Pi.Function.module EquivLike.toFunLike instEquivLike symm finTwoArrow Matrix.vecCons Matrix.vecEmpty	—	RingHomInvPair.ids
funUnique_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module EquivLike.toFunLike instEquivLike funUnique Function.eval Unique.instInhabited	—	RingHomInvPair.ids
funUnique_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module EquivLike.toFunLike instEquivLike symm funUnique AddEquiv AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Pi.instAdd AddEquiv.instEquivLike AddEquiv.symm AddEquiv.funUnique	—	RingHomInvPair.ids
piCongrLeft'_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Pi.module instEquivLike piCongrLeft'	—	RingHomInvPair.ids
piCongrLeft'_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Pi.module instEquivLike symm piCongrLeft' Equiv.piCongrLeft'	—	RingHomInvPair.ids
piCongrRight_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Pi.module EquivLike.toFunLike instEquivLike piCongrRight	—	RingHomInvPair.ids
piCongrRight_refl 📖	mathematical	—	piCongrRight refl Pi.addCommMonoid Pi.module	—	RingHomInvPair.ids
piCongrRight_symm 📖	mathematical	—	symm Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids piCongrRight	—	RingHomInvPair.ids
piCongrRight_trans 📖	mathematical	—	trans Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids piCongrRight	—	RingHomInvPair.ids RingHomCompTriple.ids
piCurry_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Pi.module EquivLike.toFunLike instEquivLike piCurry Sigma.curry	—	RingHomInvPair.ids
piCurry_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Pi.module EquivLike.toFunLike instEquivLike symm piCurry Sigma.uncurry	—	RingHomInvPair.ids
piFinTwo_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Prod.instAddCommMonoid Pi.module Prod.instModule EquivLike.toFunLike instEquivLike piFinTwo	—	RingHomInvPair.ids
piFinTwo_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.instAddCommMonoid Pi.addCommMonoid Prod.instModule Pi.module EquivLike.toFunLike instEquivLike symm piFinTwo Fin.cons finZeroElim	—	RingHomInvPair.ids
piRing_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap.module EquivLike.toFunLike instEquivLike piRing LinearMap.instFunLike Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids
piRing_symm_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module EquivLike.toFunLike instEquivLike symm piRing Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids RingHomCompTriple.ids Finset.sum_congr LinearMap.coe_sum Finset.sum_apply
sumArrowLequivProdArrow_apply_fst 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Prod.instAddCommMonoid Pi.Function.module Prod.instModule EquivLike.toFunLike instEquivLike sumArrowLequivProdArrow	—	RingHomInvPair.ids
sumArrowLequivProdArrow_apply_snd 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Prod.instAddCommMonoid Pi.Function.module Prod.instModule EquivLike.toFunLike instEquivLike sumArrowLequivProdArrow	—	RingHomInvPair.ids
sumArrowLequivProdArrow_symm_apply_inl 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.instAddCommMonoid Pi.addCommMonoid Prod.instModule Pi.Function.module EquivLike.toFunLike instEquivLike symm sumArrowLequivProdArrow	—	RingHomInvPair.ids
sumArrowLequivProdArrow_symm_apply_inr 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.instAddCommMonoid Pi.addCommMonoid Prod.instModule Pi.Function.module EquivLike.toFunLike instEquivLike symm sumArrowLequivProdArrow	—	RingHomInvPair.ids

LinearMap

Definitions

Name	Category	Theorems
compLeft 📖	CompOp	14 math math: groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, mapMatrixModule_apply, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, compLeft_apply, groupCohomology.cochainsMap_f, groupCohomology.mapCocycles₁_comp_i_apply, Rep.coindMap_hom, ker_compLeft, groupCohomology.cochainsMap_f_hom, range_compLeft, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, IsBaseChange.finitePow
const 📖	CompOp	1 math math: const_apply
diag 📖	CompOp	2 math math: proj_comp_single, single_eq_pi_diag
iInfKerProjEquiv 📖	CompOp	—
lsum 📖	CompOp	7 math math: Fintype.linearIndependent_iff', lsum_apply, Fintype.linearIndependent_iff'ₛ, lsum_single, lsum_piSingle, lsum_symm_apply, Submodule.piQuotientLift_mk
pi 📖	CompOp	23 math math: Rep.resCoindHomEquiv_apply_hom, ker_pi, det_pi, Rep.resCoindAdjunction_unit_app_hom_hom, DFinsupp.injective_pi_lapply, Ideal.pi_mkQ_surjective, Ideal.pi_tensorProductMk_quotient_surjective, pi_apply, pi_eq_zero, IsLocalizedModule.pi, ContinuousLinearMap.coe_pi, IsBaseChange.pi, Matrix.diagonal_toLin', Ideal.ker_tensorProductMk_quotient, pi_proj_comp, Submodule.pi_liftQ_eq_liftQ_pi, pi_comp, proj_pi, pi_proj, Ideal.pi_mkQ_rTensor, pi_zero, single_eq_pi_diag, AffineMap.pi_linear
proj 📖	CompOp	40 math math: Rep.resCoindHomEquiv_symm_apply_hom, ModuleCat.biproductIsoPi_inv_comp_π, toAddMonoidHom_proj, Rep.resCoindAdjunction_counit_app_hom_hom, det_pi, AffineMap.proj_linear, iInf_ker_proj, iInf_ker_proj_le_iSup_range_single, AdicCompletion.pi_apply_coe, ModuleCat.HasLimit.productLimitCone_cone_π, QuadraticMap.Ring.polarBilin_pi, lsum_apply, iSup_range_single_eq_iInf_ker_proj, proj_apply, Submodule.biInf_comap_proj, coe_proj, IsLocalizedModule.pi, IsBaseChange.pi, Matrix.proj_comp_diagLinearMap, Matrix.diagonal_toLin', pi_proj_comp, proj_pi, MultilinearMap.piFamily_single_left, pi_proj, Matrix.proj_diagonal, ModuleCat.piIsoPi_hom_ker_subtype, proj_comp_single, ModuleCat.piIsoPi_inv_kernel_ι, withSeminorms_pi, ContinuousLinearMap.coe_proj, Pi.comul_comp_proj, QuadraticMap.Ring.associated_pi, iSup_range_single_le_iInf_ker_proj, Set.Finite.convexHull_eq_image, proj_surjective, proj_comp_single_ne, Submodule.iInf_comap_proj, ModuleCat.HasLimit.productLimitCone_isLimit_lift, Matrix.entryLinearMap_eq_comp, proj_comp_single_same
single 📖	CompOp	34 math math: dotProductEquiv_symm_apply, Submodule.iSup_map_single_le, Pi.comul_comp_single, iSup_range_single, iInf_ker_proj_le_iSup_range_single, Finsupp.lcoeFun_comp_lsingle, MvPowerSeries.monomial_def, iSup_range_single_eq_iInf_ker_proj, lsum_single, Submodule.closure_coe_iSup_map_single, Matrix.ker_diagonal_toLin', Submodule.iSup_map_single, Submodule.quotientPi_symm_apply, MultilinearMap.piFamily_single_left, coe_single, pi_ext'_iff, intrinsicStar_single, proj_comp_single, single_apply, Pi.comul_single, Submodule.le_comap_single_pi, iSup_range_single_le_iInf_ker_proj, disjoint_single_single, single_eq_pi_diag, MultilinearMap.pi_ext_iff, Matrix.range_diagonal, Pi.counit_comp_single, Submodule.topologicalClosure_iSup_map_single, proj_comp_single_ne, MultilinearMap.piFamily_compLinearMap_lsingle, ker_single, lsum_symm_apply, Matrix.diagonal_comp_single, proj_comp_single_same
vecCons 📖	CompOp	2 math math: vecCons_apply, vecCons₂_apply
vecCons₂ 📖	CompOp	1 math math: vecCons₂_apply
vecEmpty 📖	CompOp	2 math math: vecEmpty_apply, vecEmpty₂_apply
vecEmpty₂ 📖	CompOp	1 math math: vecEmpty₂_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Pi.apply_single map_zero
coe_proj 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instFunLike proj Function.eval	—	—
coe_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instFunLike single Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
compLeft_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module instFunLike compLeft	—	—
const_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module instFunLike const	—	—
disjoint_single_single 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Submodule Pi.addCommMonoid Pi.module Submodule.instPartialOrder Submodule.instOrderBot iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set.instMembership range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids single	—	Disjoint.mono RingHomSurjective.ids iSup_range_single_le_iInf_ker_proj disjoint_compl_right instIsConcreteLE Disjoint.le_bot
iInf_ker_proj 📖	mathematical	—	iInf Submodule Pi.addCommMonoid Pi.module Submodule.instInfSet ker RingHom.id Semiring.toNonAssocSemiring proj Bot.bot Submodule.instBot	—	bot_unique SetLike.le_def instIsConcreteLE Submodule.mem_bot
iInf_ker_proj_le_iSup_range_single 📖	mathematical	Set Set.instHasSubset Set.univ Set.instUnion SetLike.coe Finset Finset.instSetLike	Submodule Pi.addCommMonoid Pi.module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder iInf Submodule.instInfSet Set.instMembership ker RingHom.id Semiring.toNonAssocSemiring proj iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Finset.instMembership range RingHomSurjective.ids single	—	RingHomSurjective.ids SetLike.le_def instIsConcreteLE Finset.sum_apply Pi.single_eq_same Finset.sum_eq_single Pi.single_eq_of_ne Submodule.sum_mem_biSup mem_range_self
iSup_range_single 📖	mathematical	—	iSup Submodule Pi.addCommMonoid Pi.module ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids single Top.top Submodule.instTop	—	nonempty_fintype RingHomSurjective.ids iSup_pos Finset.mem_univ top_unique LE.le.trans Eq.ge iInf_emptyset iInf_ker_proj_le_iSup_range_single Finset.coe_univ Set.union_empty subset_refl Set.instReflSubset
iSup_range_single_eq_iInf_ker_proj 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instHasSubset Set.univ Set.instUnion	iSup Submodule Pi.addCommMonoid Pi.module ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set.instMembership range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids single iInf Submodule.instInfSet ker proj	—	le_antisymm RingHomSurjective.ids iSup_range_single_le_iInf_ker_proj Set.Finite.coe_toFinset le_trans iInf_ker_proj_le_iSup_range_single iSup_mono Set.Finite.mem_toFinset le_refl
iSup_range_single_le_iInf_ker_proj 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Submodule Pi.addCommMonoid Pi.module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set.instMembership range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids single iInf Submodule.instInfSet ker proj	—	iSup_le RingHomSurjective.ids range_le_iff_comap RingHomCompTriple.ids Submodule.comap_iInf iInf_congr_Prop instIsConcreteLE proj_comp_single_ne Disjoint.le_bot zero_apply
ker_compLeft 📖	mathematical	—	ker Pi.addCommMonoid Pi.Function.module RingHom.id Semiring.toNonAssocSemiring compLeft Submodule.pi Set.univ	—	Submodule.ext
ker_pi 📖	mathematical	—	ker Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring pi iInf Submodule Submodule.instInfSet	—	Submodule.ext
ker_single 📖	mathematical	—	ker Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring single Bot.bot Submodule Submodule.instBot	—	ker_eq_bot_of_injective Pi.single_injective
lsum_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid Pi.module addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike lsum Finset.sum Finset.univ comp RingHomCompTriple.ids proj	—	RingHomInvPair.ids
lsum_piSingle 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instFunLike LinearEquiv RingHomInvPair.ids addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike lsum Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids RingHomCompTriple.ids sum_apply Finset.sum_congr apply_single Fintype.sum_pi_single'
lsum_single 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid Pi.module addCommMonoid module Pi.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction EquivLike.toFunLike LinearEquiv.instEquivLike lsum single id	—	ext RingHomInvPair.ids Pi.smulCommClass RingHomCompTriple.ids coe_sum Finset.sum_congr Finset.sum_apply Finset.univ_sum_single
lsum_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid Pi.module addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm lsum comp single	—	RingHomInvPair.ids
pi_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instFunLike pi	—	—
pi_apply_eq_sum_univ 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule instFunLike Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	pi_eq_sum_univ map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass
pi_comp 📖	mathematical	—	comp Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids pi	—	RingHomCompTriple.ids
pi_eq_zero 📖	mathematical	—	pi LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instZero	—	—
pi_ext 📖	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instFunLike Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—	toAddMonoidHom_injective AddMonoidHom.functions_ext
pi_ext' 📖	—	comp Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids single	—	—	RingHomCompTriple.ids pi_ext congr_fun
pi_ext'_iff 📖	mathematical	—	comp Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids single	—	RingHomCompTriple.ids pi_ext'
pi_ext_iff 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instFunLike Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	pi_ext
pi_proj 📖	mathematical	—	pi Pi.addCommMonoid Pi.module proj id	—	—
pi_proj_comp 📖	mathematical	—	pi comp Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids proj	—	RingHomCompTriple.ids
pi_zero 📖	mathematical	—	pi LinearMap RingHom.id Semiring.toNonAssocSemiring instZero Pi.addCommMonoid Pi.module	—	ext
proj_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instFunLike proj	—	—
proj_comp_single 📖	mathematical	—	comp Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids proj single diag	—	RingHomCompTriple.ids single_eq_pi_diag proj_pi
proj_comp_single_ne 📖	mathematical	—	comp Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids proj single LinearMap instZero	—	ext RingHomCompTriple.ids Pi.single_eq_of_ne
proj_comp_single_same 📖	mathematical	—	comp Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids proj single id	—	ext RingHomCompTriple.ids Pi.single_eq_same
proj_pi 📖	mathematical	—	comp Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids proj pi	—	RingHomCompTriple.ids
proj_surjective 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instFunLike proj	—	Function.surjective_eval Zero.instNonempty
range_compLeft 📖	mathematical	—	range Pi.addCommMonoid Pi.Function.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids compLeft Submodule.pi Set.univ	—	Submodule.ext RingHomSurjective.ids
single_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.module instFunLike single Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
single_eq_pi_diag 📖	mathematical	—	single pi diag	—	ext update_apply
sum_single_apply 📖	mathematical	—	Finset.sum Pi.addCommMonoid Finset.univ Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_apply Finset.sum_pi_single
toAddMonoidHom_proj 📖	mathematical	—	toAddMonoidHom Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring proj Pi.evalAddMonoidHom AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
update_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike Function.update	—	Function.update_self Function.update_of_ne
vecCons_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module instFunLike vecCons Matrix.vecCons	—	—
vecCons₂_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid instFunLike vecCons₂ vecCons	—	smulCommClass_self Function.smulCommClass
vecEmpty_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module instFunLike vecEmpty Matrix.vecEmpty	—	—
vecEmpty₂_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid instFunLike vecEmpty₂ vecEmpty	—	Function.smulCommClass smulCommClass_self

LinearMap.CompatibleSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	—	LinearMap.CompatibleSMul Pi.addCommMonoid Function.hasSMul Pi.Function.module	—	LinearMap.map_smul_of_tower RingHomCompTriple.ids

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi_induction 📖	mathematical	NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing PUnit.commRing PUnit.module Prod.instAddCommMonoid Prod.instModule	Pi.addCommMonoid Pi.module	—	RingHomInvPair.ids nonempty_fintype Fintype.induction_empty_option Unique.instSubsingleton PEmpty.instIsEmpty
pi_induction' 📖	mathematical	PUnit.addCommGroup PUnit.module Ring.toSemiring Prod.instAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid	Pi.addCommGroup Pi.module	—	RingHomInvPair.ids nonempty_fintype Fintype.induction_empty_option Unique.instSubsingleton PEmpty.instIsEmpty

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_span_range_single_inl_iff 📖	mathematical	—	Submodule addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Function.module Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.range single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Submodule.span_induction single_eq_of_ne add_zero MulZeroClass.mul_zero Finset.sum_apply Finset.sum_congr single_apply mul_ite mul_one Finset.sum_ite_eq Finset.sum_const_zero sum_mem Submodule.addSubmonoidClass SMulMemClass.smul_mem Submodule.smulMemClass Submodule.subset_span Set.mem_range_self

Submodule

Definitions

Name	Category	Theorems
pi 📖	CompOp	30 math math: fg_pi, pi_univ_bot, quotientPi_aux.map_smul, iSup_map_single_le, mem_pi, DFinsupp.range_mapRangeLinearMap, DirectSum.ker_lmap, biInf_comap_proj, pi_mono, Module.jacobson_pi_le, pi_empty, pi_top, quotientPi_apply, iSup_map_single, quotientPi_symm_apply, DFinsupp.ker_mapRangeLinearMap, quotientPi_aux.map_add, Subalgebra.pi_toSubsemiring, Subalgebra.coe_pi, quotientPi_aux.left_inv, LinearMap.ker_compLeft, DirectSum.range_lmap, LinearMap.range_compLeft, le_comap_single_pi, coe_pi, quotientPiLift_mk, quotientPi_aux.right_inv, topologicalClosure_iSup_map_single, iInf_comap_proj, Subalgebra.pi_toSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biInf_comap_proj 📖	mathematical	—	iInf Submodule Pi.addCommMonoid Pi.module instInfSet Set Set.instMembership comap RingHom.id Semiring.toNonAssocSemiring LinearMap.proj pi	—	ext
coe_pi 📖	mathematical	—	SetLike.coe Submodule Pi.addCommMonoid Pi.module setLike pi Set.pi	—	—
iInf_comap_proj 📖	mathematical	—	iInf Submodule Pi.addCommMonoid Pi.module instInfSet comap RingHom.id Semiring.toNonAssocSemiring LinearMap.proj pi Set.univ	—	ext
iSup_map_single 📖	mathematical	—	iSup Submodule Pi.addCommMonoid Pi.module ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.single pi Set.univ	—	nonempty_fintype RingHomSurjective.ids LE.le.antisymm iSup_map_single_le Finset.univ_sum_single sum_mem_iSup mem_map_of_mem
iSup_map_single_le 📖	mathematical	—	Submodule Pi.addCommMonoid Pi.module Preorder.toLE PartialOrder.toPreorder instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.single pi	—	iSup_le RingHomSurjective.ids map_le_iff_le_comap le_comap_single_pi
le_comap_single_pi 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder comap Pi.addCommMonoid Pi.module RingHom.id Semiring.toNonAssocSemiring LinearMap.single pi	—	mem_comap mem_pi eq_or_ne Pi.single_eq_same Pi.single_eq_of_ne AddSubmonoidClass.toZeroMemClass addSubmonoidClass
mem_pi 📖	mathematical	—	Submodule Pi.addCommMonoid Pi.module SetLike.instMembership setLike pi	—	—
pi_empty 📖	mathematical	—	pi Set Set.instEmptyCollection Top.top Submodule Pi.addCommMonoid Pi.module instTop	—	SetLike.coe_injective Set.empty_pi
pi_mono 📖	mathematical	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder	Pi.addCommMonoid Pi.module pi	—	Set.pi_mono
pi_top 📖	mathematical	—	pi Top.top Submodule instTop Pi.addCommMonoid Pi.module	—	SetLike.coe_injective Set.pi_univ
pi_univ_bot 📖	mathematical	—	pi Set.univ Bot.bot Submodule instBot Pi.addCommMonoid Pi.module	—	le_bot_iff

---

← Back to Index