OAI/NumberTheory/DukePrimeDegree/Geometry/FiniteCoordinateIndependence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Independence from one-coordinate splittings

If each real coordinate is independent of all the remaining coordinates together, finite intersections factor. Hence the joint law is the product of the coordinate laws. This is used for the abelian row conditionals.

  1. theorem OAI.DukePrimeDegree.iIndepFun_of_independent_remaining line 18
  2. theorem OAI.DukePrimeDegree.joint_law_eq_pi_of_independent_remaining line 48