Documentation Verification Report

Tautological

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

Statistics

Metric	Count
Definitions `tautological`, `R`, `tautologicalRelations`, `tautologicalRelationsSolutionEquiv`, `tautologicalSolution`, `tautologicalSolutionIsPresentationCore`	6
Theorems `tautologicalRelations_G`, `tautologicalRelations_R`, `tautologicalRelations_relation`, `tautologicalSolution_isPresentation`, `tautologicalSolution_var`, `tautological_G`, `tautological_R`, `tautological_relation`, `tautological_var`	9
Total	15

Module.Presentation

Definitions

Name	Category	Theorems
`tautological` 📖	CompOp	4 math math: `tautological_R`, `tautological_G`, `tautological_var`, `tautological_relation`
`tautologicalRelations` 📖	CompOp	5 math math: `tautologicalSolution_var`, `tautologicalRelations_R`, `tautologicalRelations_G`, `tautologicalRelations_relation`, `tautologicalSolution_isPresentation`
`tautologicalRelationsSolutionEquiv` 📖	CompOp	—
`tautologicalSolution` 📖	CompOp	2 math math: `tautologicalSolution_var`, `tautologicalSolution_isPresentation`
`tautologicalSolutionIsPresentationCore` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tautologicalRelations_G` 📖	mathematical	—	`Module.Relations.G` `tautologicalRelations`	—	—
`tautologicalRelations_R` 📖	mathematical	—	`Module.Relations.R` `tautologicalRelations` `tautological.R`	—	—
`tautologicalRelations_relation` 📖	mathematical	—	`Module.Relations.relation` `tautologicalRelations` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instSub` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Finsupp.single` `AddMonoidWithOne.toOne` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `Finsupp.instZero` `Finsupp.smulZeroClass` `DistribSMul.toSMulZeroClass` `instDistribSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction`	—	—
`tautologicalSolution_isPresentation` 📖	mathematical	—	`Module.Relations.Solution.IsPresentation` `tautologicalRelations` `tautologicalSolution`	—	`Module.Relations.Solution.IsPresentationCore.isPresentation`
`tautologicalSolution_var` 📖	mathematical	—	`Module.Relations.Solution.var` `tautologicalRelations` `tautologicalSolution`	—	—
`tautological_G` 📖	mathematical	—	`Module.Relations.G` `toRelations` `tautological`	—	—
`tautological_R` 📖	mathematical	—	`Module.Relations.R` `toRelations` `tautological` `tautological.R`	—	—
`tautological_relation` 📖	mathematical	—	`Module.Relations.relation` `toRelations` `tautological` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instSub` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Finsupp.single` `AddMonoidWithOne.toOne` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction`	—	`Finsupp.smul_single` `mul_one`
`tautological_var` 📖	mathematical	—	`Module.Relations.Solution.var` `toRelations` `tautological` `toSolution`	—	—

Module.Presentation.tautological

Definitions

Name	Category	Theorems
`R` 📖	CompData	2 math math: `Module.Presentation.tautological_R`, `Module.Presentation.tautologicalRelations_R`

---

← Back to Index