Tower

📁 Source: Mathlib/FieldTheory/Tower.lean

Statistics

Metric	Count
Definitions	0
Theorems left, right, left, right	4
Total	4

FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
left 📖	mathematical	—	Module.Finite Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Module.Finite.left
right 📖	mathematical	—	Module.Finite	—	Module.Finite.right

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
left 📖	mathematical	—	Module.Finite Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	exists_ne of_injective LinearMap.IsScalarTower.compatibleSMul' RingHomInvPair.ids AddMonoid.nat_smulCommClass' smul_left_injective IsDomain.toIsCancelMulZero
right 📖	mathematical	—	Module.Finite	—	Submodule.restrictScalars_injective Submodule.restrictScalars_top eq_top_iff Submodule.span_le Submodule.subset_span

---

← Back to Index