Documentation Verification Report

Flag

📁 Source: Mathlib/LinearAlgebra/Basis/Flag.lean

Statistics

Metric	Count
Definitions `Flag`, `flag`, `toFlag`	3
Theorems `flag_covBy`, `flag_last`, `flag_le_flag`, `flag_le_iff`, `flag_le_ker_coord`, `flag_le_ker_coord_iff`, `flag_le_ker_dual`, `flag_lt_flag`, `flag_mono`, `flag_strictMono`, `flag_succ`, `flag_wcovBy`, `flag_zero`, `isChain_range_flag`, `isMaxChain_range_flag`, `mem_toFlag`, `self_mem_flag`, `self_mem_flag_iff`, `toFlag_carrier`	19
Total	22

Module.Basis

Definitions

Name	Category	Theorems
`flag` 📖	CompOp	19 math math: `flag_le_ker_dual`, `flag_last`, `flag_mono`, `flag_zero`, `isMaxChain_range_flag`, `flag_le_ker_coord`, `flag_succ`, `flag_covBy`, `flag_lt_flag`, `flag_wcovBy`, `self_mem_flag_iff`, `flag_le_iff`, `flag_le_flag`, `self_mem_flag`, `flag_le_ker_coord_iff`, `mem_toFlag`, `toFlag_carrier`, `isChain_range_flag`, `flag_strictMono`
`toFlag` 📖	CompOp	2 math math: `mem_toFlag`, `toFlag_carrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flag_covBy` 📖	mathematical	—	`CovBy` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `flag`	—	`flag_succ` `Submodule.covBy_span_singleton_sup` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`flag_last` 📖	mathematical	—	`flag` `Top.top` `Submodule` `Submodule.instTop`	—	`Set.image_univ` `span_eq`
`flag_le_flag` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `flag`	—	`flag_mono`
`flag_le_iff` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `flag` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `Module.Basis` `instFunLike`	—	`Submodule.span_le` `Set.forall_mem_image`
`flag_le_ker_coord` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `flag` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `coord`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `flag_le_ker_coord_iff`
`flag_le_ker_coord_iff` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `flag` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `coord`	—	`RingHomInvPair.ids` `repr_self` `NeZero.one`
`flag_le_ker_dual` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `flag` `LinearMap.ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `DFunLike.coe` `Module.Basis` `Module.Dual` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instFunLike` `dualBasis` `Finite.of_fintype` `Fin.fintype`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `smulCommClass_self` `Finite.of_fintype` `coe_dualBasis` `Unique.instSubsingleton` `flag_le_ker_coord_iff` `le_refl`
`flag_lt_flag` 📖	mathematical	—	`Submodule` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `flag`	—	`flag_strictMono`
`flag_mono` 📖	mathematical	—	`Monotone` `Submodule` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Submodule.instPartialOrder` `flag`	—	`Fin.monotone_iff_le_succ` `flag_succ` `le_sup_right`
`flag_strictMono` 📖	mathematical	—	`StrictMono` `Submodule` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Submodule.instPartialOrder` `flag`	—	`Fin.strictMono_iff_lt_succ` `flag_succ`
`flag_succ` 📖	mathematical	—	`flag` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet` `DFunLike.coe` `Module.Basis` `instFunLike`	—	`Set.image_insert_eq` `Submodule.span_insert`
`flag_wcovBy` 📖	mathematical	—	`WCovBy` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `flag`	—	`CovBy.wcovBy` `flag_covBy`
`flag_zero` 📖	mathematical	—	`flag` `Bot.bot` `Submodule` `Submodule.instBot`	—	`Set.image_empty` `Submodule.span_empty`
`isChain_range_flag` 📖	mathematical	—	`IsChain` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Set.range` `flag`	—	`Monotone.isChain_range` `flag_mono`
`isMaxChain_range_flag` 📖	mathematical	—	`IsMaxChain` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Set.range` `flag`	—	`Flag.maxChain`
`mem_toFlag` 📖	mathematical	—	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Flag` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `SetLike.instMembership` `Flag.instSetLike` `toFlag` `flag`	—	—
`self_mem_flag` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `flag` `DFunLike.coe` `Module.Basis` `instFunLike`	—	`Submodule.subset_span` `Set.mem_image_of_mem`
`self_mem_flag_iff` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `flag` `DFunLike.coe` `Module.Basis` `instFunLike`	—	`self_mem_span_image`
`toFlag_carrier` 📖	mathematical	—	`SetLike.coe` `Flag` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Flag.instSetLike` `toFlag` `Set.range` `flag`	—	—

(root)

Definitions

Name	Category	Theorems
`Flag` 📖	CompData	27 math math: `Flag.coe_ofIsMaxChain`, `Flag.isMax_coe`, `Flag.coe_map`, `Flag.symm_map`, `Flag.bot_mem`, `Flag.top_mem`, `IsChain.exists_subset_flag`, `Flag.coe_covBy_coe`, `Flag.chain_le`, `Flag.exists_mem_mem`, `Flag.isMin_coe`, `Flag.exists_mem`, `Flag.grade_coe`, `Flag.mem_rangeFin`, `Flag.coe_mk`, `Flag.chain_lt`, `Flag.mem_iff_forall_le_or_ge`, `Flag.mk_coe`, `Module.Basis.mem_toFlag`, `Flag.ext_iff`, `Module.Basis.toFlag_carrier`, `Flag.mem_coe_iff`, `Flag.rangeFin_carrier`, `Flag.coe_wcovBy_coe`, `Flag.coe_smul`, `Flag.instNonempty`, `Flag.maxChain`

---

← Back to Index