OAI/Analysis/SymmetricDomains/PositiveReal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Release061.Biholomorph.WeightedLieModel.grade line 53
2. def OAI.Release061.Biholomorph.WeightedLieModel.lowerHalf line 55
3. def OAI.Release061.Biholomorph.WeightedLieModel.lowerOneSquared line 65
4. theorem OAI.Release061.Biholomorph.WeightedLieModel.lowerHalf_injective line 76
5. theorem OAI.Release061.Biholomorph.WeightedLieModel.lowerOneSquared_injective line 83
6. theorem OAI.Release061.Biholomorph.WeightedLieModel.complex_euler_trace_zero line 92
7. theorem OAI.Release061.Biholomorph.WeightedLieModel.grading_balance line 96
8. theorem OAI.Release061.Biholomorph.WeightedLieModel.lowerOneSquared_surjective line 104
9. theorem OAI.Release061.Biholomorph.WeightedLieModel.exists_positive_real line 109