MIL/C10_Linear_Algebra/S04_Bases.lean

GitHub source file

31 declarations, 2 contain sorry, 0 declared as axioms

Imports (5)
Imported by 1 file
  1. example (example at line 61) line 61 source
  2. example (example at line 67) line 67 source
  3. example (example at line 73) line 73 source
  4. example (example at line 77) line 77 source
  5. example (example at line 81) line 81 source
  6. example (example at line 84) line 84 source
  7. example (example at line 109) line 109 source
  8. example (example at line 114) line 114 source

    Source comment

    The family of vectors underlying the above basis is indeed ``b``.
    example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) (i : ι) :
    Basis.mk b_indep (fun v _ ↦ b_spans v) i = b i :=
…
  9. example (example at line 121) line 121 source
  10. example (example at line 124) line 124 source
  11. example (example at line 128) line 128 source
  12. example (example at line 132) line 132 source
  13. example (example at line 138) line 138 source
  14. example (example at line 142) line 142 source
  15. example (example at line 156) line 156 source
  16. example (example at line 159) line 159 source
  17. example (example at line 173) line 173 source
  18. example (example at line 179) line 179 source
  19. example (example at line 197) sorry line 197 source
  20. example (example at line 211) line 211 source

    Source comment

    `Fin n → K` is the archetypical space with dimension `n` over `K`.
    example (n : ℕ) : Module.finrank K (Fin n → K) = n :=
…
  21. example (example at line 215) line 215 source

    Source comment

    Seen as a vector space over itself, `ℂ` has dimension one.
    example : Module.finrank ℂ ℂ = 1 :=
…
  22. example (example at line 219) line 219 source

    Source comment

    But as a real vector space it has dimension two.
    example : Module.finrank ℝ ℂ = 2 :=
…
  23. example (example at line 223) line 223 source
  24. example (example at line 227) line 227 source
  25. example (example at line 233) line 233 source
  26. example (example at line 235) line 235 source
  27. example (example at line 244) line 244 source
  28. example (example at line 248) line 248 source
  29. example (example at line 249) sorry line 249 source
  30. example (example at line 263) line 263 source
  31. example (example at line 266) line 266 source