OAI/Computability/StarHeight/Actions.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.AffineRecovery.affine line 17
  2. lemma OAI.GeneralizedStarHeight.AffineRecovery.update_add line 20
  3. lemma OAI.GeneralizedStarHeight.AffineRecovery.update_eq_linear_add line 32
  4. theorem OAI.GeneralizedStarHeight.AffineRecovery.recovery line 38
  5. theorem OAI.GeneralizedStarHeight.AffineRecovery.recovery_height line 55
  6. abbrev OAI.GeneralizedStarHeight.RightRegular.V line 69
  7. def OAI.GeneralizedStarHeight.RightRegular.basis line 71
  8. def OAI.GeneralizedStarHeight.RightRegular.action line 73
  9. lemma OAI.GeneralizedStarHeight.RightRegular.action_basis line 76
  10. lemma OAI.GeneralizedStarHeight.RightRegular.action_one line 79
  11. lemma OAI.GeneralizedStarHeight.RightRegular.action_mul line 84
  12. lemma OAI.GeneralizedStarHeight.RightRegular.basis_injective line 90
  13. lemma OAI.GeneralizedStarHeight.RightRegular.action_faithful line 92
  14. lemma OAI.GeneralizedStarHeight.RightRegular.value_recovery line 98
  15. def OAI.GeneralizedStarHeight.Homogenization.lift line 107
  16. lemma OAI.GeneralizedStarHeight.Homogenization.lift_apply_one line 114
  17. lemma OAI.GeneralizedStarHeight.Homogenization.lift_apply_zero line 117
  18. lemma OAI.GeneralizedStarHeight.Homogenization.lift_comp line 120