Pi

📁 Source: Mathlib/LinearAlgebra/Quotient/Pi.lean

Statistics

Metric	Count
Definitions piQuotientLift, quotientPi, quotientPiLift, invFun, toFun	5
Theorems piQuotientLift_mk, piQuotientLift_single, quotientPiLift_mk, quotientPi_apply, left_inv, map_add, map_smul, right_inv, quotientPi_symm_apply	9
Total	14

Submodule

Definitions

Name	Category	Theorems
piQuotientLift 📖	CompOp	3 math math: quotientPi_symm_apply, piQuotientLift_single, piQuotientLift_mk
quotientPi 📖	CompOp	2 math math: quotientPi_apply, quotientPi_symm_apply
quotientPiLift 📖	CompOp	2 math math: quotientPi_apply, quotientPiLift_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piQuotientLift_mk 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap RingHom.id Semiring.toNonAssocSemiring	DFunLike.coe LinearMap HasQuotient.Quotient hasQuotient CommRing.toRing Pi.addCommMonoid Quotient.addCommGroup Pi.module Quotient.module LinearMap.instFunLike piQuotientLift LinearEquiv RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring EquivLike.toFunLike LinearEquiv.instEquivLike LinearMap.lsum	—	RingHomInvPair.ids smulCommClass_self piQuotientLift.eq_1 RingHomCompTriple.ids LinearMap.lsum_apply LinearMap.sum_apply mkQ_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr
piQuotientLift_single 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap RingHom.id Semiring.toNonAssocSemiring	DFunLike.coe LinearMap HasQuotient.Quotient hasQuotient CommRing.toRing Pi.addCommMonoid Quotient.addCommGroup Pi.module Quotient.module LinearMap.instFunLike piQuotientLift Pi.single Quotient.instZeroQuotient Ring.toSemiring mapQ	—	RingHomCompTriple.ids LinearMap.sum_apply Finset.sum_congr Finset.sum_eq_single Pi.single_eq_of_ne map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.mem_univ Pi.single_eq_same
quotientPiLift_mk 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker RingHom.id Semiring.toNonAssocSemiring	DFunLike.coe LinearMap HasQuotient.Quotient Pi.addCommMonoid Pi.module hasQuotient CommRing.toRing Pi.addCommGroup pi Set.univ Quotient.addCommGroup Quotient.module LinearMap.instFunLike quotientPiLift	—	—
quotientPi_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.module hasQuotient CommRing.toRing Pi.addCommGroup pi Set.univ Quotient.addCommGroup Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike quotientPi LinearMap Ring.toSemiring LinearMap.instFunLike quotientPiLift mkQ	—	RingHomInvPair.ids
quotientPi_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.module hasQuotient CommRing.toRing Pi.addCommGroup pi Set.univ Quotient.addCommGroup Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotientPi LinearMap LinearMap.instFunLike piQuotientLift LinearMap.single	—	RingHomInvPair.ids

Submodule.quotientPi_aux

Definitions

Name	Category	Theorems
invFun 📖	CompOp	2 math math: left_inv, right_inv
toFun 📖	CompOp	4 math math: map_smul, map_add, left_inv, right_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
left_inv 📖	mathematical	—	HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.module Submodule.hasQuotient CommRing.toRing Pi.addCommGroup Submodule.pi Set.univ invFun toFun	—	Submodule.Quotient.induction_on Submodule.mkQ_apply RingHomInvPair.ids smulCommClass_self Pi.smulCommClass LinearMap.lsum_single LinearMap.id_apply
map_add 📖	mathematical	—	toFun HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.module Submodule.hasQuotient CommRing.toRing Pi.addCommGroup Submodule.pi Set.univ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Submodule.Quotient.addCommGroup Pi.instAdd	—	LinearMap.map_add Eq.ge Submodule.ker_mkQ
map_smul 📖	mathematical	—	toFun HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.module Submodule.hasQuotient CommRing.toRing Pi.addCommGroup Submodule.pi Set.univ Submodule.Quotient.instSMul Pi.instSMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.id	—	LinearMap.map_smul Eq.ge Submodule.ker_mkQ
right_inv 📖	mathematical	—	HasQuotient.Quotient Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.module Submodule.hasQuotient CommRing.toRing Pi.addCommGroup Submodule.pi Set.univ invFun toFun	—	Function.rightInverse_iff_comp RingHomCompTriple.ids LinearMap.coe_comp LinearMap.id_coe LinearMap.pi_ext Finite.of_fintype Submodule.Quotient.induction_on LinearMap.comp_apply Submodule.piQuotientLift_single Submodule.mapQ_apply LinearMap.id_apply Pi.single_eq_same Pi.single_eq_of_ne Submodule.Quotient.mk_zero

---

← Back to Index