Theorem Module.Finite.left

Modification history

2026-01-13 19:40

Mathlib/FieldTheory/Tower.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Modified Module.Finite.left View on Github →

2024-09-02 16:21

Mathlib/FieldTheory/Tower.lean

chore: split FieldTheory/Tower (#15689) …

Added Module.Finite.left View on Github →