OAI/Analysis/IrrationalRotation/Model/ProductFactorStructure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.ProductModel.IsCovariantFieldRepresentation line 10

    Also declared: ComparatorChallenges/IrrationalRotation.lean:731 (same declaration text).

  2. def OAI.Invariant233.ProductModel.centralDiagonalIntegral line 20

    Also declared: ComparatorChallenges/IrrationalRotation.lean:741 (same declaration text).