Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.mem_span_singleton_trans

Modification history

2022-03-15 08:11
src/linear_algebra/basic.lean
refactor(linear_algebra/basic): split file (#12637) …
Modified submodule.mem_span_singleton_transView on Github →
2021-12-21 10:53
src/linear_algebra/basic.lean
feat(order/galois_connection, linear_algebra/basic): `x ∈ R ∙ y` is a transitive relation (#10943)
Added submodule.mem_span_singleton_transView on Github →