Basic

📁 Source: Mathlib/Algebra/Module/Presentation/Basic.lean

Statistics

Metric	Count
Definitions ofIsPresentation, ofLinearEquiv, toRelations, toSolution, G, R, Solution, IsPresentation, desc, linearEquiv, linearMapEquiv, uniq, IsPresentationCore, desc, down, fromQuotient, ofQuotient, ofπ, ofπ', postcomp, var, π, instAddCommGroupQuotient, instQuotient, map, relation, toQuotient	27
Theorems ofIsPresentation_toRelations, ofIsPresentation_toSolution, ofLinearEquiv_toRelations, ofLinearEquiv_toSolution, toIsPresentation, linearMap_ext, linearMap_ext_iff, bijective, desc_comp_π, desc_var, exact, ker_π, linearEquiv_apply, linearEquiv_symm_var, linearMapEquiv_apply, linearMapEquiv_symm_apply, of_linearEquiv, postcomp_desc, postcomp_injective, postcomp_uniq, postcomp_uniq_symm, surjective_π, uniq_symm_var, uniq_var, π_desc_apply, desc_var, isPresentation, postcomp_desc, postcomp_injective, congr_postcomp, congr_var, ext, ext_iff, fromQuotient_comp_toQuotient, fromQuotient_toQuotient, injective_fromQuotient_iff_ker_π_eq_span, isPresentation_iff, isPresentation_mk, linearCombination_var_relation, ofQuotient_fromQuotient, ofQuotient_isPresentation, ofQuotient_var, ofQuotient_π, ofπ'_var, ofπ'_π, ofπ_var, ofπ_π, postcomp_comp, postcomp_id, postcomp_var, range_π, span_relation_le_ker_π, surjective_fromQuotient_iff_surjective_π, surjective_π_iff_span_eq_top, π_comp_map, π_comp_map_apply, π_relation, π_single, ker_toQuotient, map_single, range_map, surjective_toQuotient, toQuotient_map, toQuotient_map_apply, toQuotient_relation	65
Total	92

Module.Presentation

Definitions

Name	Category	Theorems
ofIsPresentation 📖	CompOp	2 math math: ofIsPresentation_toRelations, ofIsPresentation_toSolution
ofLinearEquiv 📖	CompOp	2 math math: ofLinearEquiv_toSolution, ofLinearEquiv_toRelations
toRelations 📖	CompOp	42 math math: cokernelRelations_relation, cokernelSolution_var, directSum_var, cokernel_relation, Module.presentationFinsupp_G, cokernel_R, ofExact_G, tensor_R, finsupp_R, directSum_relation, Module.free_iff_exists_presentation, finsupp_G, ofExact_R, toIsPresentation, ofIsPresentation_toRelations, directSum_G, finsupp_var, cokernelRelations_R, tautological_R, Module.presentationFinsupp_R, ofLinearEquiv_toSolution, ofExact_relation, cokernel_var, tensor_G, CokernelData.π_lift, finsupp_relation, exteriorPower.presentation_relation, cokernel_G, tautological_G, cokernelRelations_G, tensor_relation, exteriorPower.presentation_R, tautological_var, ofExact_var, ofLinearEquiv_toRelations, directSum_R, Module.finitePresentation_iff_exists_presentation, exteriorPower.presentation_var, exteriorPower.presentation_G, tautological_relation, Module.presentationFinsupp_var, tensor_var
toSolution 📖	CompOp	13 math math: cokernelSolution_var, directSum_var, toIsPresentation, finsupp_var, ofLinearEquiv_toSolution, cokernel_var, CokernelData.π_lift, tautological_var, ofExact_var, exteriorPower.presentation_var, ofIsPresentation_toSolution, Module.presentationFinsupp_var, tensor_var

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofIsPresentation_toRelations 📖	mathematical	Module.Relations.Solution.IsPresentation	toRelations ofIsPresentation	—	—
ofIsPresentation_toSolution 📖	mathematical	Module.Relations.Solution.IsPresentation	toSolution ofIsPresentation	—	—
ofLinearEquiv_toRelations 📖	mathematical	—	toRelations ofLinearEquiv	—	RingHomInvPair.ids
ofLinearEquiv_toSolution 📖	mathematical	—	toSolution ofLinearEquiv Module.Relations.Solution.postcomp toRelations LinearEquiv.toLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid	—	RingHomInvPair.ids
toIsPresentation 📖	mathematical	—	Module.Relations.Solution.IsPresentation toRelations toSolution	—	—

Module.Relations

Definitions

Name	Category	Theorems
G 📖	CompOp	61 math math: Module.Presentation.cokernelRelations_relation, directSum_G, Solution.surjective_π_iff_span_eq_top, Module.Presentation.directSum_var, Solution.injective_fromQuotient_iff_ker_π_eq_span, Solution.surjective_fromQuotient_iff_surjective_π, Solution.IsPresentation.linearEquiv_symm_var, Module.Presentation.cokernel_relation, Module.presentationFinsupp_G, Solution.directSumEquiv_apply_var, surjective_toQuotient, Solution.fromQuotient_toQuotient, Module.Presentation.ofExact_G, Module.Presentation.tensor_R, Solution.ofQuotient_var, Module.Presentation.directSum_relation, Module.Presentation.finsupp_G, range_map, Solution.range_π, Solution.directSum_var, Module.Presentation.directSum_G, Module.Presentation.finsupp_var, map_single, Quotient.linearMap_ext_iff, Module.Presentation.ofExact_relation, tensor_R, Module.Presentation.tensor_G, Module.Presentation.CokernelData.π_lift, solutionFinsupp_var, Module.Presentation.finsupp_relation, Solution.isPresentation_iff, exteriorPower.presentation.relations_G, tensor_G, ker_toQuotient, Solution.IsPresentation.surjective_π, Module.Presentation.cokernel_G, Solution.π_comp_map, Module.Presentation.tautological_G, directSum_relation, toQuotient_map_apply, Module.Presentation.cokernelRelations_G, Module.Presentation.tensor_relation, Solution.π_relation, Solution.IsPresentation.desc_comp_π, Solution.fromQuotient_comp_toQuotient, Solution.span_relation_le_ker_π, toQuotient_relation, Module.finitePresentation_iff_exists_presentation, toQuotient_map, Solution.IsPresentation.exact, solutionFinsupp_isPresentation, exteriorPower.presentation_G, Module.Presentation.tautologicalRelations_G, Solution.π_comp_map_apply, Solution.IsPresentation.ker_π, Algebra.Presentation.differentialsRelations_G, Solution.π_single, tensor_relation, Solution.IsPresentation.π_desc_apply, Solution.linearCombination_var_relation, Solution.ofQuotient_π
R 📖	CompOp	32 math math: Solution.injective_fromQuotient_iff_ker_π_eq_span, Algebra.Presentation.differentialsRelations_R, Module.Presentation.cokernel_R, Module.Presentation.tensor_R, Module.Presentation.finsupp_R, Module.Presentation.directSum_relation, Module.free_iff_exists_presentation, range_map, Module.Presentation.ofExact_R, Module.Presentation.cokernelRelations_R, Module.Presentation.tautological_R, map_single, Module.presentationFinsupp_R, directSum_R, tensor_R, Module.Presentation.finsupp_relation, Solution.isPresentation_iff, Algebra.Presentation.differentials.comm₁₂, ker_toQuotient, Solution.π_comp_map, exteriorPower.presentation.relations_R, toQuotient_map_apply, exteriorPower.presentation_R, Solution.span_relation_le_ker_π, Module.Presentation.directSum_R, Module.Presentation.tautologicalRelations_R, Module.finitePresentation_iff_exists_presentation, toQuotient_map, Solution.IsPresentation.exact, Solution.π_comp_map_apply, Solution.IsPresentation.ker_π, Solution.ofQuotient_π
Solution 📖	CompData	6 math math: Solution.directSumEquiv_apply_var, Solution.IsPresentation.linearMapEquiv_apply, Solution.IsPresentation.linearMapEquiv_symm_apply, exteriorPower.presentation.relationsSolutionEquiv_symm_apply_var, exteriorPower.presentation.relationsSolutionEquiv_apply_apply, Solution.directSumEquiv_symm_apply_var
instAddCommGroupQuotient 📖	CompOp	17 math math: Solution.injective_fromQuotient_iff_ker_π_eq_span, Solution.surjective_fromQuotient_iff_surjective_π, Solution.IsPresentation.linearEquiv_symm_var, surjective_toQuotient, Solution.fromQuotient_toQuotient, Solution.IsPresentation.linearEquiv_apply, Solution.ofQuotient_var, Quotient.linearMap_ext_iff, ker_toQuotient, Solution.IsPresentation.bijective, toQuotient_map_apply, Solution.fromQuotient_comp_toQuotient, Solution.ofQuotient_fromQuotient, toQuotient_relation, toQuotient_map, Solution.ofQuotient_isPresentation, Solution.ofQuotient_π
instQuotient 📖	CompOp	17 math math: Solution.injective_fromQuotient_iff_ker_π_eq_span, Solution.surjective_fromQuotient_iff_surjective_π, Solution.IsPresentation.linearEquiv_symm_var, surjective_toQuotient, Solution.fromQuotient_toQuotient, Solution.IsPresentation.linearEquiv_apply, Solution.ofQuotient_var, Quotient.linearMap_ext_iff, ker_toQuotient, Solution.IsPresentation.bijective, toQuotient_map_apply, Solution.fromQuotient_comp_toQuotient, Solution.ofQuotient_fromQuotient, toQuotient_relation, toQuotient_map, Solution.ofQuotient_isPresentation, Solution.ofQuotient_π
map 📖	CompOp	8 math math: range_map, map_single, Algebra.Presentation.differentials.comm₁₂, Solution.π_comp_map, toQuotient_map_apply, toQuotient_map, Solution.IsPresentation.exact, Solution.π_comp_map_apply
relation 📖	CompOp	24 math math: Module.Presentation.cokernelRelations_relation, Algebra.Presentation.differentials.comm₁₂_single, Solution.injective_fromQuotient_iff_ker_π_eq_span, Module.Presentation.cokernel_relation, Module.Presentation.directSum_relation, range_map, map_single, Module.Presentation.ofExact_relation, Module.Presentation.finsupp_relation, Solution.isPresentation_iff, exteriorPower.presentation_relation, ker_toQuotient, directSum_relation, Module.Presentation.tensor_relation, Solution.π_relation, Solution.span_relation_le_ker_π, toQuotient_relation, Module.Presentation.tautologicalRelations_relation, Solution.IsPresentation.ker_π, Module.Presentation.tautological_relation, exteriorPower.presentation.relations_relation, tensor_relation, Solution.linearCombination_var_relation, Solution.ofQuotient_π
toQuotient 📖	CompOp	10 math math: Solution.IsPresentation.linearEquiv_symm_var, surjective_toQuotient, Solution.fromQuotient_toQuotient, Solution.ofQuotient_var, Quotient.linearMap_ext_iff, ker_toQuotient, toQuotient_map_apply, Solution.fromQuotient_comp_toQuotient, toQuotient_relation, toQuotient_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_toQuotient 📖	mathematical	—	LinearMap.ker Finsupp G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Quotient Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupQuotient Finsupp.module Semiring.toModule instQuotient RingHom.id Semiring.toNonAssocSemiring toQuotient Submodule.span Set.range R relation	—	Submodule.ker_mkQ
map_single 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp R MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing G Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike map Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne relation	—	Finsupp.linearCombination_single one_smul
range_map 📖	mathematical	—	LinearMap.range Finsupp R MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing G Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids map Submodule.span Set.range relation	—	Finsupp.range_linearCombination
surjective_toQuotient 📖	mathematical	—	Finsupp G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Quotient DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupQuotient Finsupp.module Semiring.toModule instQuotient LinearMap.instFunLike toQuotient	—	Submodule.mkQ_surjective
toQuotient_map 📖	mathematical	—	LinearMap.comp Finsupp R MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing G Quotient Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupQuotient Finsupp.module Semiring.toModule instQuotient RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids toQuotient map LinearMap LinearMap.instZero	—	Finsupp.lhom_ext' RingHomCompTriple.ids LinearMap.ext_ring map_single toQuotient_relation
toQuotient_map_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Quotient Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupQuotient Finsupp.module Semiring.toModule instQuotient LinearMap.instFunLike toQuotient R map NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	DFunLike.congr_fun RingHomCompTriple.ids toQuotient_map
toQuotient_relation 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Quotient Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupQuotient Finsupp.module Semiring.toModule instQuotient LinearMap.instFunLike toQuotient relation NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Submodule.mkQ_apply Submodule.Quotient.mk_eq_zero Submodule.subset_span

Module.Relations.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearMap_ext 📖	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Relations.Quotient AddCommGroup.toAddCommMonoid Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient LinearMap.instFunLike Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Module.Relations.toQuotient Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	Submodule.linearMap_qext Finsupp.lhom_ext' RingHomCompTriple.ids LinearMap.ext_ring
linearMap_ext_iff 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Relations.Quotient AddCommGroup.toAddCommMonoid Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient LinearMap.instFunLike Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Module.Relations.toQuotient Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	linearMap_ext

Module.Relations.Solution

Definitions

Name	Category	Theorems
IsPresentation 📖	CompData	9 math math: Algebra.Presentation.differentialsSolution_isPresentation, Module.Presentation.cokernelSolution.isPresentation, Module.Presentation.toIsPresentation, isPresentation_mk, isPresentation_iff, IsPresentationCore.isPresentation, Module.Relations.solutionFinsupp_isPresentation, ofQuotient_isPresentation, Module.Presentation.tautologicalSolution_isPresentation
IsPresentationCore 📖	CompData	—
fromQuotient 📖	CompOp	7 math math: injective_fromQuotient_iff_ker_π_eq_span, surjective_fromQuotient_iff_surjective_π, fromQuotient_toQuotient, IsPresentation.linearEquiv_apply, IsPresentation.bijective, fromQuotient_comp_toQuotient, ofQuotient_fromQuotient
ofQuotient 📖	CompOp	4 math math: ofQuotient_var, ofQuotient_fromQuotient, ofQuotient_isPresentation, ofQuotient_π
ofπ 📖	CompOp	2 math math: ofπ_π, ofπ_var
ofπ' 📖	CompOp	2 math math: ofπ'_var, ofπ'_π
postcomp 📖	CompOp	11 math math: postcomp_comp, postcomp_id, IsPresentation.linearMapEquiv_apply, postcomp_var, Module.Presentation.ofLinearEquiv_toSolution, IsPresentationCore.postcomp_desc, IsPresentation.postcomp_desc, congr_postcomp, IsPresentation.of_linearEquiv, IsPresentation.postcomp_uniq, IsPresentation.postcomp_uniq_symm
var 📖	CompOp	33 math math: ofπ'_var, Module.Presentation.cokernelSolution_var, surjective_π_iff_span_eq_top, Module.Presentation.directSum_var, IsPresentation.linearEquiv_symm_var, Module.Presentation.tautologicalSolution_var, directSumEquiv_apply_var, ofQuotient_var, postcomp_var, exteriorPower.presentation.relationsSolutionEquiv_symm_apply_var, exteriorPower.presentation.relationsSolutionEquiv_apply_apply, range_π, directSum_var, Module.Presentation.finsupp_var, directSumEquiv_symm_apply_var, IsPresentation.uniq_var, Module.Presentation.cokernel_var, Module.Relations.solutionFinsupp_var, tensor_var, isPresentation_iff, IsPresentation.uniq_symm_var, Module.Presentation.tautological_var, Module.Presentation.ofExact_var, ext_iff, ofπ_var, exteriorPower.presentation_var, congr_var, π_single, Module.presentationFinsupp_var, linearCombination_var_relation, IsPresentationCore.desc_var, Module.Presentation.tensor_var, IsPresentation.desc_var
π 📖	CompOp	22 math math: surjective_π_iff_span_eq_top, Algebra.Presentation.differentials.comm₂₃, injective_fromQuotient_iff_ker_π_eq_span, surjective_fromQuotient_iff_surjective_π, fromQuotient_toQuotient, range_π, ofπ'_π, Module.Presentation.CokernelData.π_lift, isPresentation_iff, ofπ_π, IsPresentation.surjective_π, π_comp_map, π_relation, IsPresentation.desc_comp_π, fromQuotient_comp_toQuotient, span_relation_le_ker_π, IsPresentation.exact, π_comp_map_apply, IsPresentation.ker_π, π_single, IsPresentation.π_desc_apply, ofQuotient_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_postcomp 📖	mathematical	—	postcomp	—	—
congr_var 📖	mathematical	—	var	—	—
ext 📖	—	var	—	—	—
ext_iff 📖	mathematical	—	var	—	ext
fromQuotient_comp_toQuotient 📖	mathematical	—	LinearMap.comp Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.Relations.Quotient Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Module.Relations.instAddCommGroupQuotient Finsupp.module Semiring.toModule Module.Relations.instQuotient RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids fromQuotient Module.Relations.toQuotient π	—	RingHomCompTriple.ids
fromQuotient_toQuotient 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Relations.Quotient AddCommGroup.toAddCommMonoid Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient LinearMap.instFunLike fromQuotient Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Module.Relations.toQuotient π	—	—
injective_fromQuotient_iff_ker_π_eq_span 📖	mathematical	—	Module.Relations.Quotient DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient LinearMap.instFunLike fromQuotient LinearMap.ker Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule π Submodule.span Set.range Module.Relations.R Module.Relations.relation	—	Module.Relations.ker_toQuotient RingHomCompTriple.ids fromQuotient_comp_toQuotient LinearMap.ker_comp LinearMap.ker_eq_bot Submodule.comap_bot eq_bot_iff Module.Relations.surjective_toQuotient RingHomSurjective.ids Module.Relations.range_map Module.Relations.toQuotient_map_apply
isPresentation_iff 📖	mathematical	—	IsPresentation Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid Set.range Module.Relations.G var Top.top Submodule Submodule.instTop LinearMap.ker Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring π Module.Relations.R Module.Relations.relation	—	injective_fromQuotient_iff_ker_π_eq_span surjective_π_iff_span_eq_top surjective_fromQuotient_iff_surjective_π IsPresentation.bijective
isPresentation_mk 📖	mathematical	Submodule.span Ring.toSemiring AddCommGroup.toAddCommMonoid Set.range Module.Relations.G var Top.top Submodule Submodule.instTop LinearMap.ker Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring π Module.Relations.R Module.Relations.relation	IsPresentation	—	isPresentation_iff
linearCombination_var_relation 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination var Module.Relations.relation NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
ofQuotient_fromQuotient 📖	mathematical	—	fromQuotient Module.Relations.Quotient Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient ofQuotient LinearMap.id Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Module.Relations.Quotient.linearMap_ext ofQuotient_π
ofQuotient_isPresentation 📖	mathematical	—	IsPresentation Module.Relations.Quotient Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient ofQuotient	—	ofQuotient_fromQuotient Function.bijective_id
ofQuotient_var 📖	mathematical	—	var Module.Relations.Quotient Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient ofQuotient DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Module.Relations.toQuotient Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
ofQuotient_π 📖	mathematical	—	π Module.Relations.Quotient Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient ofQuotient Submodule.mkQ Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Submodule.span Finsupp.instAddCommMonoid Set.range Module.Relations.R Module.Relations.relation	—	ofπ_π
ofπ'_var 📖	mathematical	LinearMap.comp Finsupp Module.Relations.R MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.Relations.G Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Module.Relations.map LinearMap LinearMap.instZero	var ofπ' DFunLike.coe LinearMap.instFunLike Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomCompTriple.ids
ofπ'_π 📖	mathematical	LinearMap.comp Finsupp Module.Relations.R MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.Relations.G Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Module.Relations.map LinearMap LinearMap.instZero	π ofπ'	—	RingHomCompTriple.ids ofπ_π
ofπ_var 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Module.Relations.relation NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	var ofπ Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
ofπ_π 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Module.Relations.relation NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	π ofπ	—	Finsupp.lhom_ext' LinearMap.ext_ring RingHomCompTriple.ids π_single
postcomp_comp 📖	mathematical	—	postcomp LinearMap.comp Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	RingHomCompTriple.ids
postcomp_id 📖	mathematical	—	postcomp LinearMap.id Ring.toSemiring AddCommGroup.toAddCommMonoid	—	—
postcomp_var 📖	mathematical	—	var postcomp DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	—	—
range_π 📖	mathematical	—	LinearMap.range Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids π Submodule.span Set.range var	—	Finsupp.range_linearCombination
span_relation_le_ker_π 📖	mathematical	—	Submodule Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.span Set.range Module.Relations.R Module.Relations.relation LinearMap.ker AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring π	—	Submodule.span_le π_relation
surjective_fromQuotient_iff_surjective_π 📖	mathematical	—	Module.Relations.Quotient DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient LinearMap.instFunLike fromQuotient Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule π	—	Function.Surjective.of_comp_iff Module.Relations.surjective_toQuotient
surjective_π_iff_span_eq_top 📖	mathematical	—	Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike π Submodule.span Set.range var Top.top Submodule Submodule.instTop	—	RingHomSurjective.ids LinearMap.range_eq_top range_π
π_comp_map 📖	mathematical	—	LinearMap.comp Finsupp Module.Relations.R MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.Relations.G Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids π Module.Relations.map LinearMap LinearMap.instZero	—	Finsupp.lhom_ext' RingHomCompTriple.ids LinearMap.ext_ring Module.Relations.map_single π_relation
π_comp_map_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike π Module.Relations.R Module.Relations.map NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	RingHomCompTriple.ids π_comp_map LinearMap.zero_apply
π_relation 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike π Module.Relations.relation NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	linearCombination_var_relation
π_single 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike π Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne var	—	Finsupp.linearCombination_single one_smul

Module.Relations.Solution.IsPresentation

Definitions

Name	Category	Theorems
desc 📖	CompOp	5 math math: linearMapEquiv_symm_apply, postcomp_desc, desc_comp_π, π_desc_apply, desc_var
linearEquiv 📖	CompOp	2 math math: linearEquiv_symm_var, linearEquiv_apply
linearMapEquiv 📖	CompOp	2 math math: linearMapEquiv_apply, linearMapEquiv_symm_apply
uniq 📖	CompOp	4 math math: uniq_var, uniq_symm_var, postcomp_uniq, postcomp_uniq_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective 📖	mathematical	Module.Relations.Solution.IsPresentation	Function.Bijective Module.Relations.Quotient DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient LinearMap.instFunLike Module.Relations.Solution.fromQuotient	—	—
desc_comp_π 📖	mathematical	Module.Relations.Solution.IsPresentation	LinearMap.comp Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids desc Module.Relations.Solution.π	—	Finsupp.lhom_ext' RingHomCompTriple.ids LinearMap.ext_ring Module.Relations.Solution.π_single desc_var
desc_var 📖	mathematical	Module.Relations.Solution.IsPresentation	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike desc Module.Relations.Solution.var	—	linearEquiv_symm_var Module.Relations.Solution.π_single
exact 📖	mathematical	Module.Relations.Solution.IsPresentation	Function.Exact Finsupp Module.Relations.R MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.Relations.G DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Module.Relations.map AddCommGroup.toAddCommMonoid Module.Relations.Solution.π NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	RingHomSurjective.ids LinearMap.exact_iff Module.Relations.range_map Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span bijective
ker_π 📖	mathematical	Module.Relations.Solution.IsPresentation	LinearMap.ker Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Ring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring Module.Relations.Solution.π Submodule.span Set.range Module.Relations.R Module.Relations.relation	—	bijective
linearEquiv_apply 📖	mathematical	Module.Relations.Solution.IsPresentation	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.Relations.Quotient AddCommGroup.toAddCommMonoid Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient EquivLike.toFunLike LinearEquiv.instEquivLike linearEquiv LinearMap LinearMap.instFunLike Module.Relations.Solution.fromQuotient	—	RingHomInvPair.ids
linearEquiv_symm_var 📖	mathematical	Module.Relations.Solution.IsPresentation	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.Relations.Quotient AddCommGroup.toAddCommMonoid Module.Relations.instAddCommGroupQuotient Module.Relations.instQuotient EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearEquiv Module.Relations.Solution.var LinearMap Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Module.Relations.toQuotient Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	LinearEquiv.injective RingHomInvPair.ids LinearEquiv.apply_symm_apply Module.Relations.Solution.π_single
linearMapEquiv_apply 📖	mathematical	Module.Relations.Solution.IsPresentation	DFunLike.coe Equiv LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.Relations.Solution EquivLike.toFunLike Equiv.instEquivLike linearMapEquiv Module.Relations.Solution.postcomp	—	—
linearMapEquiv_symm_apply 📖	mathematical	Module.Relations.Solution.IsPresentation	DFunLike.coe Equiv Module.Relations.Solution LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid EquivLike.toFunLike Equiv.instEquivLike Equiv.symm linearMapEquiv desc	—	—
of_linearEquiv 📖	mathematical	Module.Relations.Solution.IsPresentation	Module.Relations.Solution.postcomp LinearEquiv.toLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid	—	RingHomInvPair.ids RingHomCompTriple.ids Module.Relations.Quotient.linearMap_ext Module.Relations.Solution.π_single LinearMap.coe_comp LinearEquiv.coe_coe Function.Bijective.comp LinearEquiv.bijective bijective
postcomp_desc 📖	mathematical	Module.Relations.Solution.IsPresentation	Module.Relations.Solution.postcomp desc	—	Module.Relations.Solution.ext desc_var
postcomp_injective 📖	—	Module.Relations.Solution.IsPresentation Module.Relations.Solution.postcomp	—	—	RingHomCompTriple.ids Module.Relations.Quotient.linearMap_ext Module.Relations.Solution.π_single Module.Relations.Solution.congr_var LinearMap.ext bijective DFunLike.congr_fun
postcomp_uniq 📖	mathematical	Module.Relations.Solution.IsPresentation	Module.Relations.Solution.postcomp LinearEquiv.toLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid uniq	—	RingHomInvPair.ids postcomp_desc
postcomp_uniq_symm 📖	mathematical	Module.Relations.Solution.IsPresentation	Module.Relations.Solution.postcomp LinearEquiv.toLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid LinearEquiv.symm uniq	—	RingHomInvPair.ids postcomp_desc
surjective_π 📖	mathematical	Module.Relations.Solution.IsPresentation	Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Module.Relations.Solution.π	—	bijective
uniq_symm_var 📖	mathematical	Module.Relations.Solution.IsPresentation	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm uniq Module.Relations.Solution.var	—	RingHomInvPair.ids desc_var
uniq_var 📖	mathematical	Module.Relations.Solution.IsPresentation	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid EquivLike.toFunLike LinearEquiv.instEquivLike uniq Module.Relations.Solution.var	—	RingHomInvPair.ids desc_var
π_desc_apply 📖	mathematical	Module.Relations.Solution.IsPresentation	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike desc Finsupp Module.Relations.G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Module.Relations.Solution.π	—	DFunLike.congr_fun RingHomCompTriple.ids desc_comp_π

Module.Relations.Solution.IsPresentationCore

Definitions

Name	Category	Theorems
desc 📖	CompOp	2 math math: postcomp_desc, desc_var
down 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
desc_var 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike desc Module.Relations.Solution.var	—	Module.Relations.Solution.congr_var postcomp_desc
isPresentation 📖	mathematical	—	Module.Relations.Solution.IsPresentation	—	RingHomInvPair.ids postcomp_injective RingHomInvPair.triples₂ Module.Relations.Solution.ext desc_var Module.Relations.Solution.π_single Module.Relations.Quotient.linearMap_ext LinearEquiv.bijective
postcomp_desc 📖	mathematical	—	Module.Relations.Solution.postcomp desc	—	—
postcomp_injective 📖	—	Module.Relations.Solution.postcomp	—	—	—

---

← Back to Index