Theorem CompleteLattice.independent_of_independent_coe_Iic_comp

Modification history

2024-11-25 10:13

Mathlib/Order/SupIndep.lean

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

Deleted CompleteLattice.independent_of_independent_coe_Iic_comp View on Github →

2024-02-20 23:51

Mathlib/Order/SupIndep.lean

feat: add lemma `LinearMap.trace_restrict_eq_sum_trace_restrict` (#10638)

Added CompleteLattice.independent_of_independent_coe_Iic_comp View on Github →