OAI/GroupTheory/BooneHigman/MonoidAlgebras.lean

GitHub source file

191 declarations, 0 contain sorry, 0 declared as axioms

Finite compiler monoids, zero products, both F₂ algebras, and selector constructions.

  1. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade_le_twice_length line 15
  2. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_zero_context line 28
  3. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.left_map line 48
  4. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.right_map line 55
  5. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.ZeroProduct.test line 66
  6. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.ZeroProduct.contextual line 69
  7. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.ZeroProduct.ideal line 86
  8. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.value_context line 96
  9. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.testedClass_context line 100
  10. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.terminalAlphabet line 121
  11. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.terminalMachine line 122
  12. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteValue line 124
  13. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteClass line 127
  14. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.projection_grade line 132
  15. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteTest_eq line 137
  16. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteValue_zero line 148
  17. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteValue_context line 155
  18. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteValue_ideal line 172
  19. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteClass_context line 184
  20. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteClass_ideal line 195
  21. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteClass_nil line 202
  22. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.search_value_eq line 206
  23. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tests_bounded line 215
  24. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partialNormal_nil line 246
  25. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.contextual_zero line 253
  26. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.zeroIdeal_zero line 258
  27. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteTest_nil line 279
  28. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finite_search_nil line 288
  29. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tests_zero line 293
  30. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.group_search_value line 307
  31. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.group_tests line 312
  32. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.quota_smaller line 340
  33. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.all_budgets line 349
  34. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.exists_total_fixed_point line 369
  35. structure OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.Family line 386

    Source documentation

    The actual finite machine used uniformly in the source bootstrap. Every field is constructed below from partial recursiveness of the universal word evaluator; none is an assumption on an input group.

    structure Family where
…
  36. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.exists_family line 402
  37. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.family line 412
  38. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.source_bootstrap line 415
  39. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.base line 435
  40. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables_members line 440
  41. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables_absorb line 448
  42. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables_short line 458
  43. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables_isolateT line 477
  44. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables_staticT line 488
  45. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables_isolateG line 502
  46. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables_staticG line 518
  47. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.tuple_selected_rulesEq line 539

    Source documentation

    Every nonzero irreducible ordered tuple receives its literal selector. The finite processing stage is chosen beyond the complete selector word.

    theorem tuple_selected_rulesEq (a : Markers S) (T : ℕ → Part (List (List S × List S)))
    (bases : ℕ → List (List S × List S))
    (hT : ∀ n,∃ rs∈T n,RulesEq rs (process (a:=a) (bases n) (stages a.zero) n n))
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers, OAI.FiniteAlgebraicEnvelopes.Bootstrap.RulesEq, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.stages

  48. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.selectors_rulesEq line 594

    Source documentation

    Source selectors for the stabilized quotient, with the distinguished element first in the tuple. Not an extra algebraic assumption on that quotient.

    theorem selectors_rulesEq (a : Selectors.Markers S) (bases : ℕ → List (List S × List S))
    (hT : ∀ n,∃ rs∈T n,RulesEq rs (Selectors.process (a:=a) (bases n) (Selectors.stages a.zero) n n))
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.Markers, OAI.FiniteAlgebraicEnvelopes.Bootstrap.RulesEq, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.stages

  49. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.index line 657
  50. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.processor line 658
  51. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.index_fixed line 660
  52. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.index_good line 662
  53. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.index_budget line 665
  54. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.index_stable line 668
  55. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.wf_sigma line 672
  56. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.H line 674
  57. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.hMonoidWithZero line 676
  58. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.zero_H line 680
  59. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.one_ne_zero_H line 682
  60. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.hNontrivial line 686
  61. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.computable_wordProblem_H line 688
  62. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.selectors_H line 694
  63. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.group_code_eq_iff line 704
  64. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupEval line 720
  65. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupEval_surjective line 725
  66. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupEmbedding line 733
  67. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupEmbedding_injective line 737
  68. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.KAlphabet line 742
  69. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.KMachine line 743
  70. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.K line 744
  71. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kMonoidWithZero line 750
  72. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.zero_K line 752
  73. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.one_ne_zero_K line 754
  74. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kNontrivial line 759
  75. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finite_relations_K line 763

    Source documentation

    The displayed literal presentation for K has a finite alphabet and finitely many relators; every side of a relator has length at most four.

    theorem finite_relations_K :
    {p : List (Word.Letter Sigma (Bool×family.Γ) (ParameterMachine.State family.Q (index s h))) ×
      List (Word.Letter Sigma (Bool×family.Γ) (ParameterMachine.State family.Q (index s h))) |
        Word.Rule KAlphabet (KMachine s h) p.1 p.2}.Finite :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.Sigma, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.index, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.KAlphabet, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.KMachine

  76. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.computable_wordProblem_K line 769
  77. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.realizes_processor line 777
  78. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.copyEmbedding line 780
  79. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.copyEmbedding_injective line 784
  80. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.copyEmbedding_ne_one line 788
  81. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.copyEmbedding_ne_zero line 792
  82. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.hFG line 796
  83. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kFG line 799
  84. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupUnitsEmbedding line 802
  85. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.groupUnitsEmbedding_injective line 805
  86. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.SmallAlgebra line 810
  87. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.BigAlgebra line 811
  88. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.smallAlgebra_simple line 813
  89. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.algebraEmbedding line 816
  90. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.algebraEmbedding_injective line 819
  91. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.one_not_in_smallAlgebra line 823
  92. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.word line 837
  93. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.Rel line 839
  94. abbrev OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.Presentation line 842
  95. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.generator line 844
  96. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.word_generator line 847
  97. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.monoidEval line 856
  98. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.monoidEval_mk line 862
  99. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.monoidEval_zero line 870
  100. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.toPresentation line 875
  101. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.toPresentation_basis line 893
  102. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.monoidBasis line 897
  103. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.freeEval line 902
  104. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.freeEval_word line 905
  105. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.freeEval_respects line 916
  106. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.fromPresentation line 922
  107. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.fromPresentation_mk line 925
  108. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.from_to_basis line 936
  109. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.from_to line 944
  110. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.to_from line 954
  111. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.equivalence line 971

    Source documentation

    Exact finite algebra presentation: replace the monoid equations by the same free-algebra equations and set a representative of monoid zero equal to zero.

    def equivalence : Presentation k S rel z ≃ₐ[k] Contracted.Algebra k M :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.Presentation, OAI.FiniteAlgebraicEnvelopes.Contracted.Algebra

  112. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.finite_relations line 975
  113. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.AlgebraGenerators line 992
  114. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.AlgebraRelations line 994
  115. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.algebraPresentation line 998

    Source documentation

    The source algebra B has precisely the literal compiler equations and a zero equation.

    def algebraPresentation : RingQuot (AlgebraRelations s h k) ≃ₐ[k] BigAlgebra s h k :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.AlgebraRelations, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.BigAlgebra

  116. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.algebraRelations_finite line 1002
  117. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.algebraGenerators_finite line 1008
  118. def OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.quotientGenerators line 1016
  119. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.quotientGenerators_generate line 1018
  120. theorem OAI.FiniteAlgebraicEnvelopes.ContractedPresentation.equivalenceGenerators_generate line 1030
  121. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.bigGenerators line 1043
  122. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.bigGenerators_finite line 1046
  123. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.bigGenerators_generate line 1048
  124. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.cong line 1059

    Source documentation

    Collapse precisely the pairs whose first coordinate is zero. This quotient is the zero product (K \ {0}) × P ⊔ {0} from the algebra construction.

    def cong : Con (K × P) where
…
  125. abbrev OAI.FiniteAlgebraicEnvelopes.ZeroProduct.Mon line 1079
  126. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.pair line 1081
  127. instance OAI.FiniteAlgebraicEnvelopes.ZeroProduct.(instance at line 1083) line 1083
  128. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.pair_eq_iff line 1085
  129. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.pair_zero line 1088
  130. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.pair_eq_zero line 1091
  131. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.pair_surjective line 1099
  132. instance OAI.FiniteAlgebraicEnvelopes.ZeroProduct.(instance at line 1104) line 1104
  133. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.pair_one line 1118
  134. instance OAI.FiniteAlgebraicEnvelopes.ZeroProduct.(instance at line 1124) line 1124
  135. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.toOption line 1127

    Source documentation

    A precise normal-form identification with the set in the manuscript.

    noncomputable def toOption (a : Mon K P) : Option ({k : K // k≠0} × P) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.ZeroProduct.Mon

  136. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.fromOption line 1135
  137. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.toOption_pair line 1139
  138. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.toOption_zero line 1142
  139. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.equiv line 1146
  140. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.T line 1176
  141. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.TLetter line 1177
  142. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.TCode line 1178
  143. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.TClass line 1179
  144. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.TTest line 1180
  145. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tPairEval line 1190
  146. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tEval line 1200
  147. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tPairEval_surjective line 1203
  148. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tEval_surjective line 1210
  149. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteValue_eq_iff line 1213
  150. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteValue_eq_zero line 1221
  151. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tClass_eq_iff line 1228
  152. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tClass_eq_none line 1248
  153. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tTest_eq_class line 1255
  154. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tTest_properties line 1258
  155. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.t_code_eq_iff line 1262
  156. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kappa line 1274
  157. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kappa_injective line 1277
  158. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kappa_word line 1280
  159. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.t_normal line 1295
  160. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tTest_eq_iff line 1306
  161. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tTest_eq_none line 1310
  162. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kappa_zero line 1314
  163. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separator line 1325

    Source documentation

    The source's separator is the seventh letter, distinct from both code alphabets, all four selector markers, and the zero letter.

    def separator : H s h := Quotient.present (processor s h) [6]

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.H, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Quotient.present, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.processor

  164. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separator_avoid_T line 1327
  165. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separator_avoid_G line 1332
  166. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables_isolate_separator line 1337
  167. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separator_word line 1352
  168. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separator_nonzero line 1358
  169. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separator_injective line 1375
  170. theorem OAI.FiniteAlgebraicEnvelopes.Contracted.coefficient_map line 1404
  171. theorem OAI.FiniteAlgebraicEnvelopes.Contracted.map_injective line 1418
  172. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kappa₀ line 1430
  173. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kappaAlgebra line 1432
  174. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.kappaAlgebra_injective line 1435
  175. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.left₀ line 1446
  176. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.rightBasis line 1452
  177. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.leftAlgebra line 1461
  178. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.rightAlgebra line 1462
  179. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.leftAlgebra_basis line 1465
  180. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.rightAlgebra_single line 1469
  181. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.left_right_commute line 1476
  182. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.tensorMap line 1495
  183. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.tensorMap_basis line 1498
  184. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.nonzeroPair line 1504
  185. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.nonzeroPair_bijective line 1507
  186. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.nonzeroEquiv line 1519
  187. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.tensorBasis line 1522
  188. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.tensorLinearEquiv line 1524
  189. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.tensorMap_linear line 1527
  190. theorem OAI.FiniteAlgebraicEnvelopes.ZeroProduct.tensorMap_bijective line 1537
  191. def OAI.FiniteAlgebraicEnvelopes.ZeroProduct.tensorEquiv line 1542