Goursat

📁 Source: Mathlib/LinearAlgebra/Goursat.lean

Statistics

Metric	Count
Definitions goursatFst, goursatSnd	2
Theorems goursat, goursatFst_prod_goursatSnd_le, goursatFst_toAddSubgroup, goursatSnd_toAddSubgroup, goursat_surjective	5
Total	7

Submodule

Definitions

Name	Category	Theorems
goursatFst 📖	CompOp	3 math math: goursatFst_prod_goursatSnd_le, goursatFst_toAddSubgroup, goursat_surjective
goursatSnd 📖	CompOp	3 math math: goursatFst_prod_goursatSnd_le, goursatSnd_toAddSubgroup, goursat_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
goursat 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient hasQuotient addCommGroup Quotient.addCommGroup Quotient.module map Prod.instAddCommMonoid Prod.instModule RingHomSurjective.ids LinearMap.prodMap subtype comap mkQ LinearMap.graph LinearEquiv.toLinearMap	—	RingHomSurjective.ids RingHomCompTriple.ids LinearMap.coe_fst LinearMap.range_comp map.congr_simp range_subtype LinearMap.submoduleMap_surjective LinearMap.coe_snd RingHomInvPair.ids goursat_surjective comap_map_eq_self ext ker_mkQ goursatFst_prod_goursatSnd_le
goursatFst_prod_goursatSnd_le 📖	mathematical	—	Submodule Ring.toSemiring Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule Preorder.toLE PartialOrder.toPreorder instPartialOrder prod goursatFst goursatSnd	—	AddSubgroup.goursatFst_prod_goursatSnd_le
goursatFst_toAddSubgroup 📖	mathematical	—	toAddSubgroup goursatFst AddSubgroup.goursatFst AddCommGroup.toAddGroup Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid	—	AddSubgroup.ext neg_mem
goursatSnd_toAddSubgroup 📖	mathematical	—	toAddSubgroup goursatSnd AddSubgroup.goursatSnd AddCommGroup.toAddGroup Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid	—	AddSubgroup.ext neg_mem
goursat_surjective 📖	mathematical	Submodule Ring.toSemiring Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule SetLike.instMembership setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid module LinearMap.instFunLike subtype	LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid hasQuotient goursatFst goursatSnd Quotient.addCommGroup Quotient.module LinearMap.range Prod.instAddCommMonoid Prod.instModule SetLike.instMembership setLike addCommMonoid module RingHomSurjective.ids LinearMap.comp RingHomCompTriple.ids LinearMap.prodMap mkQ subtype LinearMap.graph LinearEquiv.toLinearMap	—	AddSubgroup.normal_goursatFst AddSubgroup.normal_goursatSnd RingHomInvPair.ids RingHomSurjective.ids RingHomCompTriple.ids AddSubgroup.goursat_surjective AddMonoidHom.mem_range smul_mem AddEquiv.map_add' Equiv.left_inv Equiv.right_inv toAddSubgroup_injective AddSubgroup.ext mem_toAddSubgroup LinearMap.mem_graph_iff

---

← Back to Index