Commit 2023-06-29 23:57 bd2fff86

View on Github →

fix precedence of Nat.iterate (#5589)

Estimated changes

modified theorem iterate_frobenius
modified theorem MonoidHom.iterate_map_div
modified theorem MonoidHom.iterate_map_inv
modified theorem MonoidHom.iterate_map_mul
modified theorem MonoidHom.iterate_map_one
modified theorem MonoidHom.iterate_map_pow
modified theorem MonoidHom.iterate_map_zpow
modified theorem RingHom.iterate_map_add
modified theorem RingHom.iterate_map_mul
modified theorem RingHom.iterate_map_neg
modified theorem RingHom.iterate_map_one
modified theorem RingHom.iterate_map_pow
modified theorem RingHom.iterate_map_smul
modified theorem RingHom.iterate_map_sub
modified theorem RingHom.iterate_map_zero
modified theorem RingHom.iterate_map_zsmul
modified theorem mul_right_iterate_apply_one
modified theorem iteratedDeriv_eq_iterate
modified theorem Complex.iter_deriv_exp
modified theorem Real.iter_deriv_exp
modified theorem Int.pred_iterate
modified theorem Int.succ_iterate
modified theorem Nat.pred_iterate
modified theorem Nat.succ_iterate
modified theorem Polynomial.expand_pow
modified theorem Set.BijOn.iterate
modified theorem Set.MapsTo.iterate
modified theorem Set.SurjOn.iterate
modified theorem Set.preimage_iterate_eq
modified theorem PreErgodic.of_iterate
modified theorem PerfectClosure.R.sound
modified theorem LinearMap.pow_apply
modified theorem Function.Bijective.iterate
modified theorem Function.Injective.iterate
modified theorem Function.Surjective.iterate
modified theorem Function.iterate_add_apply
modified theorem Function.iterate_cancel
modified theorem Function.iterate_fixed
modified theorem Function.iterate_succ_apply
modified theorem Function.iterate_zero_apply
modified theorem List.foldr_const
modified theorem Measurable.iterate
modified theorem LE.le.exists_pred_iterate
modified theorem LE.le.exists_succ_iterate
modified theorem Order.le_succ_iterate
modified theorem Order.pred_iterate_le
modified theorem exists_pred_iterate_iff_le
modified theorem exists_pred_iterate_or
modified theorem exists_succ_iterate_iff_le
modified theorem exists_succ_iterate_or
modified theorem iterate_pred_toZ
modified theorem iterate_succ_toZ
modified theorem toZ_iterate_pred
modified theorem toZ_iterate_pred_ge
modified theorem toZ_iterate_succ
modified theorem toZ_iterate_succ_le
modified theorem Ordinal.iterate_le_nfp
modified theorem Ordinal.lt_nfp
modified theorem Ordinal.nfp_le
modified theorem Ordinal.nfp_le_iff
modified theorem Continuous.iterate