Theorem CompleteLattice.independent_of_independent_coe_Iic_comp

Modification history

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_compView on Github →