Theorem Submodule.span_induction₂

Modification history

2024-11-15 15:51

Mathlib/LinearAlgebra/Span/Basic.lean

chore(LinearAlgebra/Span): split off definition of `Submodule.span` (#18618) …

Modified Submodule.span_induction₂ View on Github →

2024-10-15 22:29

Mathlib/LinearAlgebra/Span.lean

refactor: migrate to dependent induction lemmas (#17543) …

Modified Submodule.span_induction₂ View on Github →

2023-08-23 11:25

Mathlib/LinearAlgebra/Span.lean

chore: remove autoImplicit in LinearAlgebra (#6634) …

Modified Submodule.span_induction₂ View on Github →

2023-07-03 00:43

Mathlib/LinearAlgebra/Span.lean

feat: define `NonUnitalSubalgebra` and develop basic API (#5512) …

Added Submodule.span_induction₂ View on Github →