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	—	map Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike Prod.instAddCommMonoid addCommMonoid Prod.instModule module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.prodMap subtype comap HasQuotient.Quotient addCommGroup hasQuotient Quotient.addCommGroup Quotient.module mkQ LinearMap.graph LinearEquiv.toLinearMap RingHomInvPair.ids	—	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
goursatSnd_toAddSubgroup 📖	mathematical	—	toAddSubgroup goursatSnd AddSubgroup.goursatSnd AddCommGroup.toAddGroup Prod.instAddCommGroup Prod.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid	—	AddSubgroup.ext
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	LinearMap.range HasQuotient.Quotient hasQuotient goursatFst goursatSnd Quotient.addCommGroup Quotient.module RingHomSurjective.ids LinearMap.comp RingHomCompTriple.ids LinearMap.prodMap mkQ LinearMap.graph LinearEquiv.toLinearMap RingHomInvPair.ids	—	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