Theorem submodule.finrank_add_finrank_orthogonal
Modification history
2021-11-21 18:40
src/analysis/inner_product_space/projection.lean
feat(analysis/inner_product_space/projection): orthogonal group is generated by reflections (#10381)
Modified submodule.finrank_add_finrank_orthogonalView on Github →