OAI/Probability/InvariantIsing/Haar/HaarGroupTopology.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual matrix-group topology and positivity of finite Haar measure.

  1. instance OAI.InvariantIsing.specialOrthogonal_topologicalGroup line 10