Documentation Verification Report

Grassmannian

📁 Source: Mathlib/RingTheory/Grassmannian.lean

Statistics

Metric	Count
Definitions `Grassmannian`, `instCoeOutSubmodule`, `toSubmodule`, `«termG(_,_;_)»`»)	4
Theorems `ext`, `ext_iff`, `finite_quotient`, `projective_quotient`, `rankAtStalk_eq`	5
Total	9

Module

Definitions

Name	Category	Theorems
`Grassmannian` 📖	CompData	—

Module.Grassmannian

Definitions

Name	Category	Theorems
`instCoeOutSubmodule` 📖	CompOp	—
`toSubmodule` 📖	CompOp	4 math math: `rankAtStalk_eq`, `finite_quotient`, `projective_quotient`, `ext_iff`
`«termG(_,_;_)»` 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`toSubmodule`	—	—	—
`ext_iff` 📖	mathematical	—	`toSubmodule`	—	`ext`
`finite_quotient` 📖	mathematical	—	`Module.Finite` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `toSubmodule` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	—
`projective_quotient` 📖	mathematical	—	`Module.Projective` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `toSubmodule` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	—
`rankAtStalk_eq` 📖	mathematical	—	`Module.rankAtStalk` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `toSubmodule` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	—

---

← Back to Index