← all areas

Namespace Matrix 105 theorems

— 69 · GeneralLinearGroup 15 · OrthogonalGroup 1 · ProjGenLinGroup 1 · SpecialLinearGroup 18 · UnitaryGroup 1

directly in Matrix 69

• Equal trace and determinant give equal traces of all powers Matrix.trace_pow_eq_of_trace_eq_of_det_eq 0 below · cited by 2 · depth 9
• Spanning sets of Mₙ(A) lift from the residue field Matrix.span_eq_top_of_map_span_eq_top 0 below · cited by 1 · depth 10
• Spanning sets of Mₙ(k) span Mₙ(K) after base change Matrix.span_image_map_eq_top_of_span_eq_top 0 below · cited by 5 · depth 10
• Trace criterion for g⁵=1 in SL₂(R) Matrix.pow_five_eq_one_of_trace_sq_add_trace_sub_one 0 below · cited by 1 · depth 11
• Off-diagonal entries vanish under a tame matrix relation Matrix.apply_eq_zero_of_diagonal_mul_eq_pow_mul_diagonal_of_sub_one_mem 0 below · cited by 1 · depth 12
• Adapted basis for a unipotent family of 2× 2 matrices Matrix.exists_adapted_basis_of_unipotent_family 0 below · cited by 1 · depth 12
• Shape of Frobenius in a basis adapted to a nilpotent line Matrix.exists_adapted_frob_shape 0 below · cited by 1 · depth 12
• Lifting distinct residual eigenvalues of a 2×2 matrix Matrix.exists_eigenvalues_of_henselianLocalRing 0 below · cited by 1 · depth 12
• Commutant of a residually spanning set of matrices is scalar Matrix.exists_eq_smul_one_of_commute_of_map_span_eq_top 0 below · cited by 1 · depth 12
• Adapted basis for a trace-one 2×2 idempotent over a local ring Matrix.exists_mulVec_eq_and_isUnit_det_of_isIdempotentElem_of_trace_eq_one 1 below · cited by 1 · depth 12
• Determinant of a diagonal-plus-constant integer matrix Matrix.det_diagonal_add_const_int 0 below · cited by 1 · depth 13
• Trace-one 2×2 idempotents have zero determinant Matrix.det_eq_zero_of_isIdempotentElem_of_trace_eq_one 0 below · cited by 1 · depth 13
• Trace identity forces a relation between det(1-XM) and the Eᵢ Matrix.charpolyRev_mul_prod_pow_eq_prod_pow_of_forall_trace_pow_eq 0 below · cited by 1 · depth 14
• Odd irreducible two-dimensional representations span M₂ after base change Matrix.span_range_map_eq_top_of_exists_odd_of_forall_exists_mulVec_ne_smul 1 below · cited by 1 · depth 14
• Factored Cayley–Hamilton identity for 2×2 matrices Matrix.sub_smul_one_mul_sub_smul_one_eq_zero 0 below · cited by 1 · depth 14
• Hermite normal form for nonsingular integer 2×2 matrices Matrix.exists_specialLinearGroup_mul_upperTriangular 0 below · cited by 2 · depth 15
• Descent of idempotent-image and eigenspace ranks to a PID Matrix.finrank_range_and_eigenspace_of_adjoin_intCast 0 below · cited by 2 · depth 15
• Matrices commuting with a spanning set are scalar Matrix.exists_eq_smul_one_of_commute_of_span_eq_top 0 below · cited by 1 · depth 16
• Commutativity from a stable line only after base change Matrix.mul_comm_of_forall_map_mulVec_mem_span_of_forall_exists_mulVec_not_mem_span 0 below · cited by 1 · depth 16
• Elementary divisors of an integral matrix of determinant valuation 1 Matrix.exists_eq_mul_diagonal_mul_of_forall_mem_adicCompletionIntegers 1 below · cited by 8 · depth 17
• Common kernel vectors descend to the base field Matrix.exists_ne_zero_forall_mulVec_eq_zero_of_forall_map_mulVec_eq_zero 0 below · cited by 1 · depth 17
• Symplectic normal form for a unimodular alternating integer matrix Matrix.exists_transpose_mul_mul_eq_J 0 below · cited by 1 · depth 17
• Conjugation invariance of split distinct eigenvalues Matrix.hasDistinctRationalEigenvalues_of_isConj 0 below · cited by 1 · depth 17
• Coprime powers preserve distinct rational eigenvalues Matrix.hasDistinctRationalEigenvalues_pow 1 below · cited by 1 · depth 17
• Local index [O:O∩ O']=ℓ^e for diag(1,ℓ^e) Matrix.relIndex_inf_conj_diagonal_pow_eq 3 below · cited by 17 · depth 17
• Bounded ℤᵥ-stable subrings of M₂(ℚᵥ) are conjugate-integral Matrix.exists_generalLinearGroup_forall_conj_apply_mem_adicCompletionIntegers_of_subring 0 below · cited by 1 · depth 18
• Trace of powers of a 2×2 matrix as a power sum Matrix.trace_pow_eq_sum_pow 0 below · cited by 1 · depth 18
• Bounded full lattices of matrices over a PID are principal Matrix.exists_generalLinearGroup_forall_mem_addSubgroup_iff_of_isPrincipalIdealRing 0 below · cited by 2 · depth 19
• Factorisation GLₙ(ℚₚ)=GLₙ(ℤₚ)cdotGLₙ(ℚ) Matrix.exists_rat_mul_eq_map_padicInt_of_isUnit_det 1 below · cited by 1 · depth 19
• Freeness over the transposed integer subalgebra in characteristic zero Matrix.exists_bijective_transpose_mulVec_of_adjoin_intCast 0 below · cited by 1 · depth 20
• Matrices congruent to the identity over ℤₚ have unit determinant Matrix.isUnit_det_padicInt_of_norm_sub_one_lt_one 0 below · cited by 1 · depth 20
• Characteristic polynomial of a U-string matrix Matrix.charpoly_of_uString 0 below · cited by 1 · depth 21
• Existence of bifiltered p-unimodular matrices avoiding affine conditions Matrix.exists_bifiltered_unimodular_of_forall_block_avoidance 3 below · cited by 1 · depth 24
• Euler angle decomposition for SU(2) Matrix.specialUnitaryGroup_fin_two_eq_diag_mul_rotation_mul_diag 0 below · cited by 1 · depth 24
• Integer matrix with determinant prime to p has p-integral inverse Matrix.isUnit_and_padicValRat_inv_nonneg_of_not_dvd_det 0 below · cited by 1 · depth 25
• A module of order ℓ⁴ over M₂(mathbb F_ℓ) is free of rank one Matrix.nonempty_linearEquiv_self_of_natCard_eq_pow_four 0 below · cited by 3 · depth 25
• The ℓ+1 proper left ideals of M₂(𝔽_ℓ) Matrix.natCard_leftIdeal_ne_bot_ne_top_eq_and_inf_eq_bot 0 below · cited by 3 · depth 26
• Unique solution of y + D y⁽ᵖ⁾ = b for nilpotent-triangular D Matrix.existsUnique_add_mulVec_pow_eq_of_forall_mem_of_isNilpotent 0 below · cited by 1 · depth 27
• Matrices invertible modulo an ideal in the Jacobson radical Matrix.isUnit_of_isUnit_map_of_le_jacobson_bot 0 below · cited by 1 · depth 27
• Finite M₂(𝔽_ℓ)-modules have order ℓ^{2k} Matrix.exists_natCard_eq_pow_two_mul_of_module_zmod 0 below · cited by 2 · depth 28
• Lifting a left ideal of M₂(ℤ/ℓ^{e+1}) one step Matrix.exists_submodule_addEquiv_zmod_pow_succ_of_addEquiv_zmod_pow 0 below · cited by 1 · depth 28
• Finite M₂(ℤ/ℓ^m)-modules with free torsion counts are free of rank one Matrix.nonempty_linearEquiv_self_of_natCard_eq_pow_of_natCard_torsionBy 3 below · cited by 1 · depth 28
• Borel condition for stabilising a submodule of order N² Matrix.exists_algEquiv_centralizer_forall_map_le_iff_apply_one_zero_eq_zero_of_squarefree 0 below · cited by 1 · depth 29
• Rank-one freeness of M₂(ℤ/N)-modules of order N⁴ Matrix.exists_forall_existsUnique_eq_apply_of_squarefree_of_card_eq 0 below · cited by 2 · depth 29
• Trace-one, determinant-zero 2×2 matrices are rank-one projectors Matrix.isCompl_range_mulVecLin_and_invertible_of_trace_eq_one_of_det_eq_zero 0 below · cited by 2 · depth 29
• A non-trivial unipotent in SL₂(F) carrying I into I' Matrix.exists_det_eq_one_unipotent_forall_mul_mem_of_ne_bot_of_ne_top 0 below · cited by 3 · depth 30
• Unipotent in SL₂(F) stabilising I₀ and mapping I into I' Matrix.exists_det_eq_one_unipotent_forall_mul_mem_of_not_le_of_not_le 1 below · cited by 1 · depth 30
• Dimension form of Morita equivalence for Mₙ(k) Matrix.finrank_linearMap_mul_card_sq_eq_finrank_mul_finrank 0 below · cited by 1 · depth 30
• Cyclic vectors for a division algebra in M_N(K) Matrix.bijective_mulVec_and_forall_exists_mulVec_eq_of_forall_isUnit_of_finrank_eq_card 0 below · cited by 1 · depth 31
• The commutant of M_m(K)⊗ 1 consists of 1⊗ B Matrix.existsUnique_eq_one_kroneckerMap_of_forall_commute_kroneckerMap_one 0 below · cited by 1 · depth 31
• Matrices projectively commuting with SL₂(ℤ/q) are scalar Matrix.exists_eq_smul_one_of_forall_specialLinearGroup_mul_eq_smul_mul 0 below · cited by 2 · depth 31
• Every K-algebra endomorphism of Mₙ(K) is inner Matrix.exists_generalLinearGroup_forall_algHom_apply_eq_conj 0 below · cited by 2 · depth 31
• Integral M₂-representations over a valuation ring are standard Matrix.exists_generalLinearGroup_forall_conj_algHom_apply_eq_kroneckerMap_one_of_forall_apply_mem_valuationSubring 0 below · cited by 1 · depth 31
• Holomorphic intertwiner line for a holomorphic family Matrix.exists_differentiableOn_det_ne_zero_forall_intertwiner_eq_smul 0 below · cited by 1 · depth 32
• Iwahori conjugation failure transfers to the twin maximal order Matrix.exists_iwahori_conj_diagonal_not_mem_of_exists_iwahori_conj_not_mem 1 below · cited by 2 · depth 32
• Iwasawa decomposition of GLₙ(ℝ): A = b o Matrix.exists_upperTriangular_pos_diag_mul_orthogonal_eq_of_det_ne_zero 0 below · cited by 4 · depth 32
• Iwahori conjugation by Y⁻¹ lands in M₂(ℤₚ) Matrix.forall_iwahori_conj_mem_of_exists_iwahori_conj_not_mem 1 below · cited by 1 · depth 32
• Smooth QR factorisation on GLₙ(ℝ) Matrix.exists_contDiffOn_upperTriangular_pos_diag_mul_orthogonal_eq 0 below · cited by 2 · depth 33
• Prescribing determinants mod two distinct primes Matrix.exists_det_map_eq_of_isUnit_of_ne 0 below · cited by 2 · depth 33
• Iwahori double cosets at determinant valuation one Matrix.exists_eq_iwahori_mul_diagonal_mul_iwahori_or_eq_atkinLehner_mul_of_mem_iwahori 0 below · cited by 2 · depth 33
• Whitehead's lemma for diag(g₁,g₂) over M₂(F) Matrix.exists_list_prod_elementary_eq_diagonal_of_det_map_mul_eq_one 0 below · cited by 1 · depth 33
• O(n)-finite continuous functions are polynomials in the entries Matrix.exists_mvPolynomial_eval_eq_of_continuousOn_orthogonal_of_finite_span_translates 0 below · cited by 2 · depth 33
• Order of GL₂(ℤ/p) Matrix.natCard_GL_fin_two_zmod_eq 0 below · cited by 5 · depth 33
• Annihilation of the constant term of a matrix pencil Matrix.aeval_const_term_eq_zero_of_forall_pos 0 below · cited by 1 · depth 34
• Uniform Vandermonde inversion bound for vector-valued coefficients Matrix.exists_const_forall_norm_le_mul_of_norm_sum_pow_smul_le 0 below · cited by 2 · depth 34
• Conjugation invariance of the quadratic and cubic trace tensors of mathfrakgl₃ Matrix.sum_apply_conj_single_eq_sum_apply_single 0 below · cited by 1 · depth 34
• Transferring lattice-saturation between two embeddings into Mₙ(ℚₚ) Matrix.exists_forall_exists_eq_pow_smul_map_coe_of_injective_of_forall_exists_eq_map_coe 0 below · cited by 1 · depth 35
• Integer two-sided inverse modulo n for a matrix with unit determinant Matrix.exists_isUnit_det_and_mul_map_castRingHom_zmod_eq_one 0 below · cited by 2 · depth 37
• Two eigenspaces of a 2× 2 matrix are lines iff both determinants vanish Matrix.finrank_ker_eq_one_and_iff_det_eq_zero_and_of_mul_eq_zero 0 below · cited by 1 · depth 37

Matrix.GeneralLinearGroup 15

• Surjectivity of a GL₂(𝔽₃)-representation from unipotents and irreducibility Matrix.GeneralLinearGroup.surjective_of_isUnipotent_of_forall_exists_mulVec_ne_smul_of_det_surjective 0 below · cited by 1 · depth 9
• Subgroups of GL₂(𝔽₃) of order ≤ 24 with full determinant Matrix.GeneralLinearGroup.card_subgroup_dvd_sixteen_of_forall_det_of_card_le_fin_two_zmod_three 0 below · cited by 1 · depth 11
• Deligne–Serre: uniform bound for few characteristic polynomials Matrix.GeneralLinearGroup.exists_natCard_le_of_isSemisimpleRepresentation_of_card_image_charpoly_le 3 below · cited by 1 · depth 15
• Dickson's theorem for finite irreducible subgroups of GL₂ Matrix.GeneralLinearGroup.exists_subfield_specialLinearGroup_conj_le_of_dvd_card 4 below · cited by 1 · depth 16
• Conjugation-stable integral matrices force g ∈ K^× GLₙ(𝒪) Matrix.GeneralLinearGroup.exists_forall_inv_mul_apply_mem_and_mul_inv_apply_mem_of_forall_conj_apply_mem 0 below · cited by 7 · depth 17
• Integral Cartan decomposition at a place over ℓ Matrix.GeneralLinearGroup.exists_eq_mul_diagonal_natCast_pow_mul_of_forall_mem_adicCompletionIntegers 1 below · cited by 12 · depth 19
• Cartan decomposition of GL₂(K) over a valuation subring Matrix.GeneralLinearGroup.exists_eq_smul_mul_diagonal_mul_of_valuationSubring 0 below · cited by 2 · depth 19
• Haar measure on GL₂(F) is right invariant Matrix.GeneralLinearGroup.isMulRightInvariant_of_isHaarMeasure_fin_two 1 below · cited by 2 · depth 22
• Semi-normaliser of the Iwahori order in GL₂(K) Matrix.GeneralLinearGroup.exists_inv_mul_mem_iwahori_or_atkinLehner_inv_mul_mem_of_forall_conj_mem 0 below · cited by 1 · depth 23
• Unimodularity and inversion invariance of Haar measure on GL₂(F) Matrix.GeneralLinearGroup.isMulRightInvariant_and_isInvInvariant_of_isHaarMeasure_fin_two 1 below · cited by 32 · depth 23
• Unimodularity of GL₂(F): the modular character is trivial Matrix.GeneralLinearGroup.modularCharacter_fin_two_eq_one 0 below · cited by 2 · depth 23
• Selberg's lemma for finitely generated subgroups of GLₙ(K) Matrix.GeneralLinearGroup.exists_normal_relIndex_ne_zero_forall_isOfFinOrder_imp_eq_one_of_fg 2 below · cited by 1 · depth 31
• Selberg's torsion-killing lemma: two primes force g=1 Matrix.GeneralLinearGroup.eq_one_of_isOfFinOrder_of_forall_sub_one_mem_of_ne 0 below · cited by 1 · depth 32
• Compact bound on conjugates of t from conjugates of t² Matrix.GeneralLinearGroup.exists_isCompact_forall_conj_mem_of_conj_mul_self_mem_of_trace_ne_zero 0 below · cited by 2 · depth 32
• Uniform Hilbert 90 for GL₂(ℂ)/GL₂(ℝ) Matrix.GeneralLinearGroup.exists_isCompact_forall_exists_map_star_eq_and_eq_mul_of_inv_mul_map_star_mem 0 below · cited by 1 · depth 33

Matrix.OrthogonalGroup 1

• Right-finite continuous functions on O(2) are polynomials in the entries Matrix.OrthogonalGroup.exists_polynomial_eq_of_continuous_of_rightFinite 0 below · cited by 1 · depth 23

Matrix.ProjGenLinGroup 1

• Selberg's lemma for PGLₙ in characteristic zero Matrix.ProjGenLinGroup.exists_torsionFree_normal_subgroup_finiteIndex_of_fg_charZero 3 below · cited by 1 · depth 30

Matrix.SpecialLinearGroup 18

• Primitive upper-triangular matrices of determinant N in one double coset Matrix.SpecialLinearGroup.exists_eq_mul_diagonal_mul_of_gcd_eq_one 0 below · cited by 1 · depth 13
• Free basis modulo ± 1 for torsion-free ΓleSL₂(ℤ) Matrix.SpecialLinearGroup.exists_generators_free_mod_neg_one_of_forall_trace_ne 6 below · cited by 1 · depth 13
• Elliptic-orbit bound for finite-index subgroups of SL₂(ℤ) Matrix.SpecialLinearGroup.finrank_addMonoidHom_add_card_orbitRelQuotient_S_ST_le_index_add_one 3 below · cited by 1 · depth 14
• Free image in PSL₂(ℤ) of a torsion-free congruence-type subgroup Matrix.SpecialLinearGroup.nonempty_freeGroupBasis_map_quotient_center_of_forall_trace_ne 5 below · cited by 4 · depth 14
• Sum-zero functions on cusps realised by homomorphisms of Γ Matrix.SpecialLinearGroup.exists_addMonoidHom_conj_T_pow_minimalPeriod_eq_of_finsum_eq_zero 2 below · cited by 1 · depth 15
• Dickson's theorem, root-group form, in odd characteristic Matrix.SpecialLinearGroup.exists_subfield_forall_upperElem_mem_iff_of_finite 3 below · cited by 1 · depth 17
• Finite-order elements of SL₂(ℤ) have trace squared at most 4 Matrix.SpecialLinearGroup.trace_sq_le_four_of_isOfFinOrder 0 below · cited by 1 · depth 17
• Number of Sylow p-subgroups of a finite subgroup of SL₂(K) Matrix.SpecialLinearGroup.card_sylow_eq_card_add_one_of_finite 2 below · cited by 1 · depth 18
• SL₂(K) is generated by torus, shears and Weyl element Matrix.SpecialLinearGroup.closure_diagonal_unipotent_weyl_eq_top 0 below · cited by 2 · depth 18
• Borel orbit structure for a finite subgroup of SL₂ Matrix.SpecialLinearGroup.borel_orbit_structure_of_sylow_eq_upper 1 below · cited by 1 · depth 19
• Tori of a finite subgroup of SL₂(K) Matrix.SpecialLinearGroup.centralizer_semisimple_structure_of_finite 0 below · cited by 2 · depth 19
• Dimension of Hom(Γ,K) for elliptic-free ΓleSL₂(ℤ) Matrix.SpecialLinearGroup.finrank_addMonoidHom_eq_of_forall_trace_ne 6 below · cited by 1 · depth 19
• Normal subgroups of SL₂(K) for |K|≥ 4 Matrix.SpecialLinearGroup.eq_top_of_normal_of_exists_ne_one_ne_neg_one 0 below · cited by 2 · depth 23
• Membership in ⟨ Γ, -1⟩ inside SL₂(ℤ) Matrix.SpecialLinearGroup.mem_sup_zpowers_neg_one_iff 0 below · cited by 8 · depth 24
• Double-coset counts for torsion-free subgroups of SL₂(ℤ) Matrix.SpecialLinearGroup.three_mul_natCard_doubleCoset_eq_index_and_two_mul_of_forall_smul_eq 0 below · cited by 2 · depth 24
• Order of SL₂(ℤ/p) is p(p²-1) Matrix.SpecialLinearGroup.natCard_fin_two_zmod_eq_of_prime 0 below · cited by 1 · depth 30
• Simultaneous lift to SL₂(ℤ) for coprime moduli Matrix.SpecialLinearGroup.exists_map_eq_and_map_eq_of_coprime 1 below · cited by 6 · depth 32
• Unit scalars on primitive vectors of (ℤ/m)² come from SL₂(ℤ) Matrix.SpecialLinearGroup.exists_int_reduce_apply_eq_units_smul_of_addOrderOf_eq 2 below · cited by 1 · depth 35

Matrix.UnitaryGroup 1

• Right-finite continuous functions on U(2) are polynomial Matrix.UnitaryGroup.exists_polynomial_eq_of_continuous_of_rightFinite 0 below · cited by 5 · depth 23