OAI/RepresentationTheory/Torus/ConvexWeights.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Invariant products from convex relations among integral characters.

  1. def OAI.ExactOrders.Partial.realVector line 12
  2. lemma OAI.ExactOrders.Partial.rational_barycentric_coordinates line 14
  3. theorem OAI.ExactOrders.Partial.zero_mem_rational_convexHull line 81
  4. lemma OAI.ExactOrders.Partial.natural_common_denominator line 108
  5. lemma OAI.ExactOrders.Partial.integral_weight_relation line 130
  6. def OAI.ExactOrders.Partial.character line 171
  7. lemma OAI.ExactOrders.Partial.character_zero line 176
  8. lemma OAI.ExactOrders.Partial.character_add line 180
  9. lemma OAI.ExactOrders.Partial.character_nsmul line 184
  10. lemma OAI.ExactOrders.Partial.character_sum line 191
  11. theorem OAI.ExactOrders.Partial.invariant_product_of_integral_relation line 200
  12. theorem OAI.ExactOrders.Partial.invariant_of_zero_mem_convexHull line 230