Basic

Statistics

Metric	Count
Definitions	0
Theorems `algebraMap_end_bijective_of_isAlgClosed`, `finrank_eq_one_of_isMulCommutative`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_end_bijective_of_isAlgClosed` 📖	mathematical	—	`Function.Bijective` `Module.End` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Module.End.instSemiring` `RingHom.instFunLike` `algebraMap` `Module.End.instAlgebra` `IsScalarTower.to_smulCommClass'` `Algebra.toSMul`	—	`IsScalarTower.to_smulCommClass'` `Module.Finite.of_injective` `smulCommClass_self` `isNoetherian_linearMap` `isNoetherian_of_isNoetherianRing_of_finite` `instIsNoetherian` `instIsSimpleModule` `LinearMap.IsScalarTower.compatibleSMul` `LinearMap.restrictScalars_injective` `IsAlgClosed.algebraMap_bijective_of_isIntegral` `DivisionRing.isDomain` `Algebra.IsAlgebraic.isIntegral` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`finrank_eq_one_of_isMulCommutative` 📖	mathematical	—	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid`	—	`nontrivial` `exists_ne` `IsScalarTower.to_smulCommClass'` `smulCommClass_self` `algebraMap_end_bijective_of_isAlgClosed` `Submodule.smul_mem` `IsSimpleOrder.eq_bot_or_eq_top` `toIsSimpleOrder` `Eq.le` `Submodule.mem_span_singleton_self` `finrank_eq_one_iff_of_nonzero` `top_le_iff`

---