OAI/Geometry/TamingCompatibility/Hodge/HodgeStarNormalGauge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pullCoefficient_intertwines line 22
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledA_intertwines line 38
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledB_intertwines line 43
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalFirst_commutes line 48
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalGauge_commutes line 60
6. lemma OAI.TamingCompatibility.UnitaryFrame.unitary_star_angular line 79
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalGauge_zero line 110
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalGauge_angular line 115
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.compact_normalGauge_angular line 125