← all areas

Namespace Nat 6 theorems

• Squarefree values of c² + D Nat.exists_squarefree_sq_add 0 below · cited by 1 · depth 13
• Divisor sums over all divisors of n determine the summands Nat.eq_of_forall_dvd_sum_divisors_eq 0 below · cited by 1 · depth 24
• Eventual equality in Macaulay's growth bound Nat.exists_forall_eq_macaulayPow_of_forall_le_macaulayPow 0 below · cited by 6 · depth 32
• Maximal Macaulay growth forces polynomial behaviour Nat.exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow 0 below · cited by 2 · depth 33
• Green's numerical lemma for Macaulay pseudo-powers Nat.macaulayPow_add_add_le_macaulayPow_add_of_le_add 0 below · cited by 1 · depth 35
• Macaulay's pseudo-power a ↦ a^{⟨ d⟩} is strictly increasing Nat.macaulayPow_lt_macaulayPow_of_lt 0 below · cited by 2 · depth 35