← all areas

Namespace AddMonoidHom 19 theorems

— 18 · IsDualPair 1

directly in AddMonoidHom 18

• An f-stable cyclic subgroup of order M from a split quadratic relation AddMonoidHom.exists_isAddCyclic_natCard_eq_forall_apply_mem_of_apply_apply_eq_smul 0 below · cited by 1 · depth 18
• A uniform exponent killing solutions of a₀+Fa₁=Fa₀+a₁=0 AddMonoidHom.exists_pos_forall_nsmul_eq_zero_of_add_eq_zero_of_finite_fixedPoints_comp_self 0 below · cited by 4 · depth 19
• Cartier–Serre bound: C-fixed vectors in a K-subspace AddMonoidHom.natCard_le_pow_finrank_of_apply_eq_self_of_map_pow_smul 0 below · cited by 3 · depth 19
• Isotropic subgroups of a left-nondegenerate pairing: #K² ≤ #V AddMonoidHom.natCard_sq_le_of_isotropic 0 below · cited by 1 · depth 19
• Completing a point of order N to a basis of A[N] AddMonoidHom.exists_addOrderOf_apply_eq_forall_apply_mem_zmultiples_of_ker_eq_zmultiples 0 below · cited by 1 · depth 20
• Surjectivity on m-torsion when the kernel is m-divisible AddMonoidHom.exists_nsmul_eq_zero_and_apply_eq_of_surjective_of_forall_ker 0 below · cited by 1 · depth 22
• Kernel orders multiply along a surjection AddMonoidHom.natCard_ker_comp_eq_mul_of_surjective 0 below · cited by 1 · depth 22
• Finiteness of the kernel of a push–pull operator on M× M AddMonoidHom.finite_setOf_pushPull_eq_zero 0 below · cited by 1 · depth 25
• Adjoint endomorphisms under a perfect pairing have equinumerous kernels AddMonoidHom.natCard_ker_eq_natCard_ker_of_pairing_adjoint 0 below · cited by 1 · depth 26
• Base change of additive duals for finite ℤₚ-modules AddMonoidHom.exists_linearEquiv_tensorProduct_zmod_addMonoidHom_apply_tmul_of_moduleFinite_padicInt 0 below · cited by 1 · depth 27
• Counting criterion for surjectivity onto q-torsion AddMonoidHom.mem_range_of_smul_eq_zero_of_natCard_ker_mul_le_of_natCard_mul_le 0 below · cited by 1 · depth 29
• Integer eigenvalues of a quadratic endomorphism annihilate c²-tc+1 AddMonoidHom.sub_mul_add_one_smul_eq_zero_of_comp_self_sub_smul_add_eq_zero_of_apply_eq_smul 0 below · cited by 1 · depth 30
• Triviality of unit-root F-crystals over W(k), k algebraically closed AddMonoidHom.exists_basis_apply_eq_self_of_map_smul_eq_frobenius_smul_of_isAlgClosed 1 below · cited by 2 · depth 32
• Quadratic relations for the six words in a dicyclic pair AddMonoidHom.exists_comp_self_sub_smul_add_eq_zero_of_dicyclic_relations_of_char_three_words 0 below · cited by 1 · depth 32
• Quadratic relations for twelve words in σ,i,j AddMonoidHom.exists_comp_self_sub_smul_add_eq_zero_of_quaternionic_relations_of_char_two_words 0 below · cited by 1 · depth 32
• Frobenius-semilinear injections have a basis of fixed vectors AddMonoidHom.exists_basis_apply_eq_self_of_map_smul_eq_pow_smul_of_isAlgClosed 0 below · cited by 1 · depth 33
• Symplectic normal form for finite abelian groups with alternating pairing AddMonoidHom.exists_addEquiv_prod_addMonoidHom_forall_apply_eq_sub_of_alternating_of_nondegenerate 0 below · cited by 1 · depth 34
• Fixed vectors span the stable part of a p⁻¹-semilinear map AddMonoidHom.coe_span_setOf_apply_eq_self_eq_setOf_forall_mem_range_iterate_of_map_smul_eq_frobeniusEquiv_symm_smul 0 below · cited by 1 · depth 35

AddMonoidHom.IsDualPair 1

• Dual pairs of degree coprime to q transport q-torsion-freeness AddMonoidHom.IsDualPair.forall_q_zsmul_eq_zero_of_isCoprime 0 below · cited by 1 · depth 16