LinearMaps

📁 Source: Mathlib/Algebra/CharP/LinearMaps.lean

Statistics

Metric	Count
Definitions	0
Theorems charP_end, instCharPLinearMapSubtypeMemSubringCenterId, instExpCharLinearMapSubtypeMemSubringCenterId	3
Total	3

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charP_end 📖	mathematical	Ideal.torsionOf CommSemiring.toSemiring Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	CharP LinearMap RingHom.id AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne End.instSemiring	—	smulCommClass_self Nat.cast_smul_eq_nsmul nsmul_eq_mul mul_one LinearMap.ext_iff CharP.cast_eq_zero_iff zero_smul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCharPLinearMapSubtypeMemSubringCenterId 📖	mathematical	—	CharP LinearMap Subring DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subring.instField RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subring.instModuleSubtypeMem Semiring.toModule Ring.toSemiring AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.End.instRing Ring.toAddCommGroup	—	charP_of_injective_ringHom smulCommClass_self IsScalarTower.left RingHom.injective DivisionRing.isSimpleRing Module.End.instNontrivial IsSimpleRing.instNontrivial
instExpCharLinearMapSubtypeMemSubringCenterId 📖	mathematical	—	ExpChar LinearMap Subring DivisionRing.toRing SetLike.instMembership Subring.instSetLike Subring.center DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subring.instField RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subring.instModuleSubtypeMem Semiring.toModule Ring.toSemiring AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.End.instRing Ring.toAddCommGroup	—	expChar_of_injective_ringHom smulCommClass_self IsScalarTower.left RingHom.injective DivisionRing.isSimpleRing Module.End.instNontrivial IsSimpleRing.instNontrivial

---

← Back to Index