OAI/NumberTheory/PiExponent/LocalAlgebra/WeightedChartRingEvaluation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.WeightedChartRingEvaluation.chart_pullback line 27
2. theorem OAI.PiExponent.WeightedChartRingEvaluation.evalAway_polyToChart line 51
3. abbrev OAI.PiExponent.WeightedChartRingEvaluation.ambientOpen line 71
4. def OAI.PiExponent.WeightedChartRingEvaluation.ambientRingEquiv line 74
5. def OAI.PiExponent.WeightedChartRingEvaluation.chartFactor line 81
6. theorem OAI.PiExponent.WeightedChartRingEvaluation.chartFactor_comp line 91
7. theorem OAI.PiExponent.WeightedChartRingEvaluation.ambient_chart_pullback line 105
8. theorem OAI.PiExponent.WeightedChartRingEvaluation.chartFactor_pullback line 132