Documentation Verification Report

Irreducible

📁 Source: Mathlib/RepresentationTheory/Irreducible.lean

Statistics

Metric	Count
Definitions `IsIrreducible`	1
Theorems `algebraMap_intertwiningMap_bijective_of_isAlgClosed`, `bijective_or_eq_zero`, `finrank_eq_one_of_isMulCommutative`, `injective_or_eq_zero`, `instIsSimpleModuleMonoidAlgebraAsModule`, `irreducible_iff_isSimpleModule_asModule`, `isSimpleModule_iff_irreducible_ofModule`, `is_simple_module_iff_irreducible_ofModule`	8
Total	9

Representation

Definitions

Name	Category	Theorems
`IsIrreducible` 📖	MathDef	3 math math: `isSimpleModule_iff_irreducible_ofModule`, `irreducible_iff_isSimpleModule_asModule`, `is_simple_module_iff_irreducible_ofModule`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_iff_isSimpleModule_asModule` 📖	mathematical	—	`IsIrreducible` `IsSimpleModule` `MonoidAlgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidAlgebra.ring` `DivisionRing.toRing` `Field.toDivisionRing` `asModule` `Semifield.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommGroupAsModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleMonoidAlgebraAsModule`	—	`isSimpleModule_iff` `OrderIso.isSimpleOrder_iff`
`isSimpleModule_iff_irreducible_ofModule` 📖	mathematical	—	`IsSimpleModule` `MonoidAlgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidAlgebra.ring` `DivisionRing.toRing` `Field.toDivisionRing` `IsIrreducible` `RestrictScalars` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RestrictScalars.module` `MonoidAlgebra.semiring` `AddCommGroup.toAddCommMonoid` `MonoidAlgebra.algebra` `Algebra.id` `ofModule`	—	`isSimpleModule_iff` `OrderIso.isSimpleOrder_iff`
`is_simple_module_iff_irreducible_ofModule` 📖	mathematical	—	`IsSimpleModule` `MonoidAlgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidAlgebra.ring` `DivisionRing.toRing` `Field.toDivisionRing` `IsIrreducible` `RestrictScalars` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RestrictScalars.module` `MonoidAlgebra.semiring` `AddCommGroup.toAddCommMonoid` `MonoidAlgebra.algebra` `Algebra.id` `ofModule`	—	`isSimpleModule_iff_irreducible_ofModule`

Representation.IsIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_intertwiningMap_bijective_of_isAlgClosed` 📖	mathematical	—	`Function.Bijective` `Representation.IntertwiningMap` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Representation.IntertwiningMap.instSemiring` `RingHom.instFunLike` `algebraMap` `Representation.IntertwiningMap.instAlgebra`	—	`IsScalarTower.to_smulCommClass'` `Representation.instIsScalarTowerMonoidAlgebraAsModule` `IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed` `instIsSimpleModuleMonoidAlgebraAsModule` `Representation.instFiniteAsModule` `Function.Bijective.of_comp_iff'` `AlgEquiv.bijective`
`bijective_or_eq_zero` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `Representation.IntertwiningMap` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `Representation.IntertwiningMap.instFunLike` `Representation.IntertwiningMap.instZero`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass'` `Representation.instIsScalarTowerMonoidAlgebraAsModule` `LinearEquiv.map_eq_zero_iff` `LinearMap.bijective_or_eq_zero` `instIsSimpleModuleMonoidAlgebraAsModule`
`finrank_eq_one_of_isMulCommutative` 📖	mathematical	—	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid`	—	`mul_comm` `IsSimpleModule.finrank_eq_one_of_isMulCommutative` `Representation.instIsScalarTowerMonoidAlgebraAsModule` `instIsSimpleModuleMonoidAlgebraAsModule` `Representation.instFiniteAsModule`
`injective_or_eq_zero` 📖	mathematical	—	`DFunLike.coe` `Representation.IntertwiningMap` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `Representation.IntertwiningMap.instFunLike` `Representation.IntertwiningMap.instZero`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass'` `Representation.instIsScalarTowerMonoidAlgebraAsModule` `LinearEquiv.map_eq_zero_iff` `LinearMap.injective_or_eq_zero` `instIsSimpleModuleMonoidAlgebraAsModule`
`instIsSimpleModuleMonoidAlgebraAsModule` 📖	mathematical	—	`IsSimpleModule` `MonoidAlgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidAlgebra.ring` `DivisionRing.toRing` `Field.toDivisionRing` `Representation.asModule` `Semifield.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Representation.instAddCommGroupAsModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Representation.instModuleMonoidAlgebraAsModule`	—	`Representation.irreducible_iff_isSimpleModule_asModule`

---

← Back to Index