← all areas

Namespace TaylorWiles 7 theorems

• Unit root separation yields an eigen-idempotent for a 2× 2 matrix TaylorWiles.exists_isEigenIdempotent_of_isUnit 2 below · cited by 1 · depth 12
• The idempotent v(M-b) for a split 2× 2 matrix TaylorWiles.isEigenIdempotent_smul_sub 1 below · cited by 1 · depth 13
• Descended character satisfies ξ(π g)=χ(g) TaylorWiles.tameDescentChar_comp_eq 0 below · cited by 1 · depth 13
• Seed element in the kernel of the cyclotomic character TaylorWiles.exists_mem_ker_cycloChar_hasDistinctRationalEigenvalues 1 below · cited by 1 · depth 14
• Trace-zero centraliser of a split regular matrix is a line TaylorWiles.finrank_inf_traceZero_of_hasDistinctRationalEigenvalues 0 below · cited by 1 · depth 14
• Existence of Taylor–Wiles primes avoiding a finite set TaylorWiles.exists_isTaylorWilesPrime 20 below · cited by 1 · depth 15
• Existence of Taylor–Wiles primes from Frobenius density TaylorWiles.exists_isTaylorWilesPrime_of_statement 3 below · cited by 1 · depth 16