Free

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

Statistics

Metric	Count
Definitions solutionFinsupp, isPresentationCore, presentationFinsupp	3
Theorems free, solutionFinsupp_isPresentation, solutionFinsupp_var, free_iff_exists_presentation, presentationFinsupp_G, presentationFinsupp_R, presentationFinsupp_var	7
Total	10

Module

Definitions

Name	Category	Theorems
presentationFinsupp 📖	CompOp	3 math math: presentationFinsupp_G, presentationFinsupp_R, presentationFinsupp_var

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
free_iff_exists_presentation 📖	mathematical	—	Free Ring.toSemiring AddCommGroup.toAddCommMonoid IsEmpty Relations.R Presentation.toRelations	—	free_def UnivLE.small UnivLE.self RingHomInvPair.ids PEmpty.instIsEmpty Relations.Solution.IsPresentation.free Presentation.toIsPresentation
presentationFinsupp_G 📖	mathematical	—	Relations.G Presentation.toRelations Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule presentationFinsupp	—	—
presentationFinsupp_R 📖	mathematical	—	Relations.R Presentation.toRelations Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule presentationFinsupp	—	—
presentationFinsupp_var 📖	mathematical	—	Relations.Solution.var Presentation.toRelations Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule presentationFinsupp Presentation.toSolution Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—

Module.Relations

Definitions

Name	Category	Theorems
solutionFinsupp 📖	CompOp	2 math math: solutionFinsupp_var, solutionFinsupp_isPresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
solutionFinsupp_isPresentation 📖	mathematical	—	Solution.IsPresentation Finsupp G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule solutionFinsupp	—	Solution.IsPresentationCore.isPresentation
solutionFinsupp_var 📖	mathematical	—	Solution.var Finsupp G MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule solutionFinsupp Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—

Module.Relations.Solution.IsPresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
free 📖	mathematical	Module.Relations.Solution.IsPresentation	Module.Free Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Module.Free.of_equiv Module.Free.finsupp Module.Free.self Module.Relations.solutionFinsupp_isPresentation

Module.Relations.solutionFinsupp

Definitions

Name	Category	Theorems
isPresentationCore 📖	CompOp	—

---

← Back to Index