← all areas

Namespace MonoidHom 12 theorems

• Mod m cyclotomic character has open kernel MonoidHom.isOpen_ker_of_cycloCharSpec 0 below · cited by 4 · depth 11
• Residually trivial character descends along a p'-order kernel MonoidHom.exists_eq_comp_of_forall_val_sub_one_mem_maximalIdeal_of_coprime_card_ker 3 below · cited by 1 · depth 12
• Characters trivial mod 𝔪 vanish on invertible-order elements MonoidHom.apply_eq_one_of_sub_one_mem_maximalIdeal_of_pow_eq_one 1 below · cited by 1 · depth 13
• Equal Frobenius traces force equal determinants in characteristic ≠ 2 MonoidHom.det_eq_of_trace_eq_of_exists_isFrobeniusAt_conj 0 below · cited by 1 · depth 13
• Conjugation invariance of characteristic polynomials of a representation MonoidHom.charpoly_apply_mul_mul_inv 0 below · cited by 2 · depth 14
• Descent of a sum of two characters to two dimensions MonoidHom.exists_finrank_two_trace_eq_add_det_eq_mul_of_mem_range 0 below · cited by 1 · depth 14
• Absolutely irreducible 2-dimensional ρ is regular semisimple on N MonoidHom.exists_mem_trace_sq_ne_four_mul_det_of_isCyclic_quotient 0 below · cited by 1 · depth 15
• Characters separate points; proper character subgroups have non-trivial annihilator MonoidHom.forall_eq_one_imp_eq_zero_and_exists_ne_zero_forall_mem_apply_eq_one 0 below · cited by 3 · depth 17
• Twisted mod p cyclotomic character: Frobenius and conjugation values MonoidHom.exists_galoisCharacter_apply_complexConjugation_eq_apply_frobenius_eq_natCast_mul 3 below · cited by 3 · depth 18
• Multiplicativity of the n-th power index in an exact sequence MonoidHom.index_range_powMonoidHom_eq_mul_of_exact 0 below · cited by 2 · depth 19
• Transfer is natural in the coefficient group MonoidHom.map_transfer_eq_transfer_comp 0 below · cited by 1 · depth 22
• Co-restricting a bimultiplicative pairing to a subfield MonoidHom.exists_subfield_units_coe_eq 0 below · cited by 1 · depth 23