Theorem Ideal.CompleteLattice.Independent.linear_independent'

Modification history

2023-08-10 19:52

Mathlib/Algebra/Module/Torsion.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Ideal.CompleteLattice.Independent.linear_independent'View on Github →

2023-05-26 05:11

Mathlib/Algebra/Module/Torsion.lean

feat: port Algebra.Module.Torsion (#4365)

Added Ideal.CompleteLattice.Independent.linear_independent'View on Github →