OAI/Analysis/CircleDomains/Sobolev/ComplexTangentFrame.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The tangent and its quarter-turn form an invertible real planar frame.

  1. def OAI.CircleDomainRigidity.complexTangentFrame line 11
  2. lemma OAI.CircleDomainRigidity.complexTangentFrame_apply line 15
  3. lemma OAI.CircleDomainRigidity.complexTangentFrame_eq_mul line 18
  4. lemma OAI.CircleDomainRigidity.complexTangentFrame_bijective line 24