MIL/C10_Linear_Algebra/S02_Subspaces.lean

GitHub source file

31 declarations, 4 contain sorry, 0 declared as axioms

Imports (4)
Imported by 1 file
  1. example (example at line 10) line 10 source
  2. example (example at line 14) line 14 source
  3. example (example at line 19) line 19 source
  4. def preimage sorry line 36 source

    depends on sorry what this means

    Statement uses: Field, AddCommGroup, Module, LinearMap, RingHom.id, Submodule

    Proof uses: Submodule.mk, AddSubmonoid.mk, AddSubsemigroup.mk, Set.preimage, sorryAx, Lean.Name, Membership.mem, Set, HAdd.hAdd, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat, HSMul.hSMul

    29 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C10_Linear_Algebra/solutions/Solutions_S02_Subspaces.lean:21 (same statement text; different proof or body). Qualify references as preimage@path.

    Tactic trace: 11 steps

    Open to load the checked before-and-after goal states.

  5. example (example at line 46) line 46 source
  6. example (example at line 48) line 48 source
  7. example (example at line 50) line 50 source
  8. example (example at line 53) line 53 source
  9. example (example at line 57) line 57 source
  10. example (example at line 59) line 59 source
  11. example (example at line 63) line 63 source

    Source comment

    If two subspaces are in direct sum then they span the whole space.
    example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊔ V = ⊤ := h.sup_eq_top
  12. example (example at line 67) line 67 source

    Source comment

    If two subspaces are in direct sum then they intersect only at zero.
    example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊓ V = ⊥ := h.inf_eq_bot
…
  13. example (example at line 75) line 75 source

    Source comment

    If subspaces are in direct sum then they span the whole space.
    example (U : ι → Submodule K V) (h : DirectSum.IsInternal U) :
  ⨆ i, U i = ⊤ := h.submodule_iSup_eq_top
  14. example (example at line 79) line 79 source

    Source comment

    If subspaces are in direct sum then they pairwise intersect only at zero.
    example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V) (h : DirectSum.IsInternal U)
    {i j : ι} (hij : i ≠ j) : U i ⊓ U j = ⊥ :=
…
  15. example (example at line 89) line 89 source

    Source comment

    The relation with external direct sums: if a family of subspaces is in internal direct sum then the map from their external direct sum into `V` is a linear isomorphism.
    noncomputable example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V)
    (h : DirectSum.IsInternal U) : (⨁ i, U i) ≃ₗ[K] V :=
…
  16. example (example at line 94) line 94 source
  17. example (example at line 97) line 97 source
  18. example (example at line 100) sorry line 100 source
  19. example (example at line 123) line 123 source
  20. example (example at line 125) line 125 source
  21. example (example at line 131) line 131 source
  22. example (example at line 133) line 133 source
  23. example (example at line 139) sorry line 139 source
  24. example (example at line 145) line 145 source
  25. example (example at line 147) line 147 source
  26. example (example at line 149) line 149 source
  27. example (example at line 151) line 151 source
  28. example (example at line 153) line 153 source
  29. example (example at line 155) line 155 source
  30. example (example at line 157) line 157 source
  31. example (example at line 165) sorry line 165 source