Namespace Pencil 5 theorems
- Root-of-unity covector through v, large on a weighted family
Pencil.exists_rootOfUnity_torus_covector_ne_zero_sum_log_ge6 below · cited by 1 · depth 19 - Algebraic covector form of the pencil mean-value inequality
Pencil.exists_covector_sum_log_ge_of_ringHom8 below · cited by 1 · depth 20 - Orthogonal covector bound by the 2×2 minors of v,w
Pencil.norm_dotProduct_mul_sup_le0 below · cited by 1 · depth 20 - All 2×2 minors bounded by twice the largest row
Pencil.norm_minor_le_two_mul_sup_minor_row0 below · cited by 2 · depth 20 - Root-of-unity covector in a pencil with large weighted logarithmic size
Pencil.exists_rootOfUnity_torus_covector_sum_log_ge6 below · cited by 1 · depth 21