Documentation Verification Report

Schur

📁 Source: Mathlib/CategoryTheory/Preadditive/Schur.lean

Statistics

Metric	Count
Definitions `fieldEndOfFiniteDimensional`, `instDivisionRingEndOfHasKernelsOfSimple`	2
Theorems `endomorphism_simple_eq_smul_id`, `finrank_endomorphism_eq_one`, `finrank_endomorphism_simple_eq_one`, `finrank_hom_simple_simple`, `finrank_hom_simple_simple_eq_one_iff`, `finrank_hom_simple_simple_eq_zero_iff`, `finrank_hom_simple_simple_eq_zero_of_not_iso`, `finrank_hom_simple_simple_le_one`, `isIso_iff_nonzero`, `isIso_of_hom_simple`, `mono_of_nonzero_from_simple`	11
Total	13

CategoryTheory

Definitions

Name	Category	Theorems
`fieldEndOfFiniteDimensional` 📖	CompOp	—
`instDivisionRingEndOfHasKernelsOfSimple` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`endomorphism_simple_eq_smul_id` 📖	mathematical	—	`Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Preadditive.homGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Linear.homModule` `CategoryStruct.id`	—	`finrank_eq_one_iff_of_nonzero'` `id_nonzero` `finrank_endomorphism_simple_eq_one`
`finrank_endomorphism_eq_one` 📖	mathematical	`IsIso`	`Module.finrank` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Linear.homModule`	—	`IsIso.id` `finrank_eq_one` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `nontrivial_of_ne` `spectrum.nonempty_of_isAlgClosed_of_finiteDimensional` `Algebra.algebraMap_eq_smul_one` `sub_eq_zero` `isUnit_iff_isIso` `IsUnit.sub_iff` `spectrum.mem_iff`
`finrank_endomorphism_simple_eq_one` 📖	mathematical	—	`Module.finrank` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Linear.homModule`	—	`finrank_endomorphism_eq_one` `isIso_iff_nonzero`
`finrank_hom_simple_simple` 📖	mathematical	`FiniteDimensional` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Field.toDivisionRing` `Preadditive.homGroup` `Linear.homModule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring`	`Module.finrank` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Iso`	—	`finrank_hom_simple_simple_eq_one_iff` `finrank_hom_simple_simple_eq_zero_iff` `not_nonempty_iff`
`finrank_hom_simple_simple_eq_one_iff` 📖	mathematical	—	`Module.finrank` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Linear.homModule` `Iso`	—	`finrank_eq_one_iff'` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `isIso_iff_nonzero` `finrank_hom_simple_simple_le_one` `Module.finrank_pos_iff_exists_ne_zero` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Iso.isIso_hom`
`finrank_hom_simple_simple_eq_zero_iff` 📖	mathematical	—	`Module.finrank` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Linear.homModule` `IsEmpty` `Iso`	—	`not_nonempty_iff` `finrank_hom_simple_simple_eq_one_iff` `finrank_hom_simple_simple_le_one`
`finrank_hom_simple_simple_eq_zero_of_not_iso` 📖	mathematical	—	`Module.finrank` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Linear.homModule`	—	`Module.finrank_zero_of_subsingleton` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `isIso_iff_nonzero`
`finrank_hom_simple_simple_le_one` 📖	mathematical	—	`Module.finrank` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Preadditive.homGroup` `Linear.homModule`	—	`subsingleton_or_nontrivial` `Module.finrank_zero_of_subsingleton` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `zero_le_one` `Nat.instZeroLEOneClass` `nontrivial_iff_exists_ne` `finrank_le_one` `commRing_strongRankCondition` `isIso_iff_nonzero` `endomorphism_simple_eq_smul_id` `Linear.smul_comp` `Category.id_comp` `Category.assoc` `IsIso.inv_hom_id` `Category.comp_id` `eq_whisker`
`isIso_iff_nonzero` 📖	mathematical	—	`IsIso`	—	`id_nonzero` `IsIso.hom_inv_id` `inv.congr_simp` `Limits.zero_comp` `isIso_of_hom_simple`
`isIso_of_hom_simple` 📖	mathematical	—	`IsIso`	—	`isIso_of_mono_of_nonzero` `mono_of_nonzero_from_simple`
`mono_of_nonzero_from_simple` 📖	mathematical	—	`Mono`	—	`Preadditive.mono_of_kernel_zero` `Limits.HasKernels.has_limit` `kernel_zero_of_nonzero_from_simple`

---

← Back to Index