MIL/C10_Linear_Algebra/solutions/Solutions_S02_Subspaces.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)
  1. example (example at line 10) line 10 source
  2. example (example at line 14) line 14 source
  3. def preimage line 21 source

    standard axioms: Quot.sound, propext what this means

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

    Proof uses: Submodule.mk, AddSubmonoid.mk, AddSubsemigroup.mk, Set.preimage

    21 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 45 steps

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

  4. example (example at line 37) line 37 source
  5. example (example at line 74) line 74 source
  6. example (example at line 76) line 76 source
  7. example (example at line 82) line 82 source
  8. example (example at line 93) line 93 source
  9. example (example at line 95) line 95 source
  10. example (example at line 97) line 97 source
  11. example (example at line 99) line 99 source
  12. example (example at line 101) line 101 source
  13. example (example at line 103) line 103 source
  14. example (example at line 105) line 105 source
  15. example (example at line 113) line 113 source