OAI/RingTheory/DirectFiniteness/DirectionFrame.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame line 13
  2. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.d line 24
  3. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.exc line 30
  4. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.u line 32
  5. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.W line 34
  6. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.D line 36
  7. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.U line 38
  8. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.exceptional line 40
  9. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.d_apply line 42
  10. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.exc_apply line 43
  11. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.u_apply line 44
  12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.d_injective line 46
  13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.exc_injective line 50
  14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.w_e_disjoint line 54
  15. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.u_injective line 57
  16. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.two_generic_E line 72

    Source documentation

    Coordinate separation for the sum of two generic vectors.

    lemma two_generic_E {j k : R × Q} (a b : Q × E)
    (he : F.u j a + F.u k b = 0) :
    F.e j a.2 + (if k = j then F.e k b.2 else 0) = 0 := by
…
  17. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.U_disjoint line 90
  18. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.generic_eq_w_E_zero line 120
  19. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.W_disjoint line 137
  20. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.U_inf_W_same line 140
  21. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.U_W_disjoint line 148
  22. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.U_exceptional_disjoint line 157
  23. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.exceptional_disjoint line 171
  24. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.card_U line 179
  25. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.card_D line 184
  26. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.card_W line 188