Theorem Ideal.CompleteLattice.Independent.linear_independent'

Modification history

2024-11-25 10:13

Mathlib/Algebra/Module/Torsion.lean

chore: rename `CompleteLattice.Independent`/`.SetIndependent` to `iSupIndep`/`sSupIndep` (#19409) …

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

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 →