OAI/NumberTheory/PiExponent/Ampleness/ReesFixedPower.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.ReesFrozenPower.map_power_eq line 14
2. theorem OAI.PiExponent.ReesFrozenPower.coordinate_mem_power line 26
3. theorem OAI.PiExponent.ReesFrozenPower.inverse_map_power_eq line 35
4. theorem OAI.PiExponent.ReesFrozenPower.inverse_mem_power line 42
5. def OAI.PiExponent.ReesFrozenPower.powerEquiv line 51
6. theorem OAI.PiExponent.ReesFrozenPower.powerEquiv_apply line 60
7. def OAI.PiExponent.ReesFrozenPower.pieceEquiv line 65
8. theorem OAI.PiExponent.ReesFrozenPower.coordinate_pieceEquiv line 69