← all areas

Namespace QuaternionAlgebra 302 theorems

— 94 · IsDefiniteRamifiedExactlyAt 2 · IsEichlerOrder 50 · IsIndefiniteRamifiedExactlyAt 8 · IsMaximalOrder 92 · IsOrder 56

directly in QuaternionAlgebra 94

• Definite quaternion algebra ramified at q with Eichler order of level N QuaternionAlgebra.exists_isDefiniteRamifiedExactlyAt_isEichlerOrder 45 below · cited by 3 · depth 15
• Finiteness of the adelic class set at a congruence level QuaternionAlgebra.finite_classSet_congruenceLevel 6 below · cited by 7 · depth 15
• Normalised connecting idele between two maximal orders QuaternionAlgebra.exists_conjByFiniteIdele_eq_mem_finiteAdeleBox_smul_inv_mem_of_relIndex_eq 30 below · cited by 5 · depth 16
• Normal form n=n₀z for a level-Nq Eichler idele QuaternionAlgebra.exists_eq_mul_mem_primeHeckeSet_mem_normalizer_meetOrder_eq_of_isEichlerOrder_meetOrder 33 below · cited by 1 · depth 16
• Existence of a definite rational quaternion algebra ramified exactly at q QuaternionAlgebra.exists_isDefiniteRamifiedExactlyAt 17 below · cited by 1 · depth 16
• Indefinite quaternion algebra ramified at q,q' with Eichler order QuaternionAlgebra.exists_isIndefiniteRamifiedExactlyAt_isMaximalOrder_isEichlerOrder_splitting 38 below · cited by 1 · depth 16
• Existence of a maximal ℤ-order in (a,bℚ) QuaternionAlgebra.exists_isMaximalOrder 0 below · cited by 3 · depth 16
• A q-sandwich bound for prime Hecke elements QuaternionAlgebra.smul_inv_mul_mem_finiteAdeleBox_of_mem_primeHeckeSet_of_inv_mul_mul_mem 3 below · cited by 1 · depth 16
• Indefinite rational quaternion algebra ramified exactly at q,q' QuaternionAlgebra.exists_indefinite_forall_isUnit_adicCompletion_iff_mem_or_mem 10 below · cited by 1 · depth 17
• Definite quaternion algebra over ℚ ramified exactly at q≡ 1 (mod 8) QuaternionAlgebra.exists_isDefiniteRamifiedExactlyAt_of_mod_eight_eq_one 13 below · cited by 1 · depth 17
• Local normal form of an idele in the Tₚ Hecke set QuaternionAlgebra.exists_ringEquiv_localBox_iff_evalAt_eq_diagonal_mul_of_mem_primeHeckeSet 14 below · cited by 18 · depth 17
• Base change of a quaternion algebra through an S-algebra model QuaternionAlgebra.exists_ringEquiv_tensorProduct_forall_one_tmul_of_algEquiv 0 below · cited by 64 · depth 17
• Integral normalisation of a local conjugating element QuaternionAlgebra.exists_units_mem_localBox_nsmul_inv_mem_forall_mem_localBox_iff_of_generalLinearGroup_conj 0 below · cited by 1 · depth 17
• Normaliser or elementary divisors (1,ℓ) for a local conjugation QuaternionAlgebra.forall_conj_mem_iff_or_exists_eq_mul_one_tmul_of_forall_conj_natCast_mul_mem 1 below · cited by 1 · depth 17
• Division algebra iff anisotropic norm form for H[K,a,b] QuaternionAlgebra.forall_isUnit_iff_forall_normForm_eq_zero 0 below · cited by 19 · depth 17
• Local division-algebra criterion via anisotropy of the norm form QuaternionAlgebra.forall_tensorProduct_adicCompletion_isUnit_iff_forall_normForm_eq_zero 2 below · cited by 26 · depth 17
• Definite quaternion algebra (-1,-q) ramified exactly at q QuaternionAlgebra.isDefiniteRamifiedExactlyAt_neg_one_neg_of_mod_four_eq_three 12 below · cited by 1 · depth 17
• Hamilton quaternions over ℚ: definite, ramified exactly at 2 QuaternionAlgebra.isDefiniteRamifiedExactlyAt_neg_one_neg_one_two 11 below · cited by 1 · depth 17
• The quaternion algebra (-2,-q) over ℚ for q≡ 5 (mod 8) QuaternionAlgebra.isDefiniteRamifiedExactlyAt_neg_two_neg_of_mod_eight_eq_five 12 below · cited by 1 · depth 17
• Isotropic quaternion algebras over K are split QuaternionAlgebra.nonempty_algEquiv_matrix_of_normForm_eq_zero 0 below · cited by 30 · depth 17
• Connecting idele of an Eichler order of level N has index N² QuaternionAlgebra.relIndex_ofFiniteIdele_mul_eq_sq_of_mem_finiteAdeleBox_of_relIndex_inf_conjByFiniteIdele_eq 38 below · cited by 1 · depth 17
• Roots of X²-tX+n in a definite quaternion algebra QuaternionAlgebra.exists_isQuadraticDatum_of_sq_lt_four_mul_of_not_isSquare_padic 6 below · cited by 3 · depth 18
• Sub-lattices of type m are the primitive ones of index N² QuaternionAlgebra.exists_ofFiniteIdele_mul_eq_ofFiniteIdele_mul_mul_iff_relIndex_eq_sq_and_forall_not_le_zsmul 51 below · cited by 1 · depth 18
• Prime Hecke factorisation of a level-N connecting idèle QuaternionAlgebra.exists_primeHeckeSet_list_prod_mul_eq_of_mem_finiteAdeleBox_of_relIndex_inf_conjByFiniteIdele_eq 37 below · cited by 1 · depth 18
• The reduced-norm unit ball is a ℤₚ-order QuaternionAlgebra.exists_subalgebra_coe_eq_setOf_norm_nrd_le_one_fg_span_eq_top_of_forall_isUnit 1 below · cited by 3 · depth 18
• Primitivity of a normalised connecting idele at level N QuaternionAlgebra.forall_inv_smul_not_mem_finiteAdeleBox_of_mem_of_smul_inv_mem_of_relIndex_inf_conjByFiniteIdele_eq 33 below · cited by 3 · depth 18
• Nine integrality relations for a prime Hecke idele at q QuaternionAlgebra.inv_mul_mem_finiteAdeleBox_and_smul_mul_mem_of_mem_primeHeckeSet_of_conjByFiniteIdele_meetOrder_eq 22 below · cited by 1 · depth 18
• Quaternion algebra with a non-zero non-unit splits QuaternionAlgebra.nonempty_algEquiv_matrix_of_ne_zero_of_not_isUnit 1 below · cited by 6 · depth 18
• Uniqueness of the definite rational quaternion algebra ramified at q QuaternionAlgebra.nonempty_algEquiv_of_isDefiniteRamifiedExactlyAt_of_prime 15 below · cited by 1 · depth 18
• Base change of a quaternion algebra to a completion of ℚ QuaternionAlgebra.nonempty_tensorProduct_adicCompletion_ringEquiv 0 below · cited by 1 · depth 18
• Ultrametric inequality for the reduced norm on a p-adic quaternion division algebra QuaternionAlgebra.norm_nrd_add_le_max_of_forall_isUnit 1 below · cited by 3 · depth 18
• Index of a left translate of M₂(ℤᵥ) QuaternionAlgebra.relIndex_map_mulLeft_eq_pow_of_eq_mul_diagonal_pow_mul 0 below · cited by 2 · depth 18
• Conjugate scaled lattices: right unit versus left unit QuaternionAlgebra.star_image_smul_eq_mulRight_image_star_image_smul_iff 0 below · cited by 1 · depth 18
• Rank-four ℤ-domains split away from p are maximal orders QuaternionAlgebra.exists_isDefiniteRamifiedExactlyAt_isMaximalOrder_range_eq_of_forall_prime_ne 19 below · cited by 1 · depth 19
• Quaternion algebra splits when b=u²-av² QuaternionAlgebra.nonempty_algEquiv_matrix_of_eq_mul_self_sub 0 below · cited by 1 · depth 19
• Reduced trace is integral when the reduced norm is, in a p-adic division quaternion algebra QuaternionAlgebra.norm_trd_le_one_of_forall_isUnit_of_norm_nrd_le_one 0 below · cited by 2 · depth 19
• Embeddings of a maximal order into a maximal order are onto QuaternionAlgebra.range_eq_of_isMaximalOrder_of_range_eq_of_range_subset 0 below · cited by 1 · depth 19
• Local index ℓⁿ of an Eichler order in a maximal order QuaternionAlgebra.relIndex_eq_pow_of_forall_mem_iff_conj_diagonal_integral 0 below · cited by 1 · depth 19
• Division quaternion algebra split away from p is definite QuaternionAlgebra.isDefiniteRamifiedExactlyAt_of_split_away_of_forall_isUnit 11 below · cited by 1 · depth 20
• Maximality of an order split away from p and p-saturated QuaternionAlgebra.isMaximalOrder_of_forall_prime_ne_of_range_eq 2 below · cited by 1 · depth 20
• Image of a finite free ℤ-algebra is a quaternion order QuaternionAlgebra.isOrder_toIntSubmodule_range_comp_includeRight 0 below · cited by 1 · depth 20
• Away from p, the ℚᵥ-base change is not division QuaternionAlgebra.not_forall_isUnit_tensorProduct_adicCompletion_of_forall_prime_ne 0 below · cited by 1 · depth 20
• Multiplicativity of the reduced norm on H[R,a,b] QuaternionAlgebra.nrd_mul 0 below · cited by 29 · depth 20
• Triviality criterion for the projective image of a quaternion unit QuaternionAlgebra.projGenLinGroup_mk_unitsMap_eq_one_iff 0 below · cited by 7 · depth 20
• Determinant in a matrix chart equals the reduced norm QuaternionAlgebra.det_ringEquiv_tmul_one_eq_algebraMap_nrd 0 below · cited by 1 · depth 21
• Stability of the prime Hecke set under h↦ℓ̂ h⁻¹ QuaternionAlgebra.mem_primeHeckeSet_iff_finiteIdeleDiagonal_mul_inv_mem 0 below · cited by 4 · depth 21
• Reduced Cayley–Hamilton identity in H[R,a,b] QuaternionAlgebra.sq_sub_trd_mul_add_nrd 0 below · cited by 3 · depth 21
• Rigidity for γ ≡ 1 mod ℓ in a definite quaternion algebra QuaternionAlgebra.exists_eq_smul_one_of_pow_eq_smul_one_of_eq_one_add_smul 2 below · cited by 1 · depth 22
• Hecke set at a good prime is a single double coset QuaternionAlgebra.primeHeckeSet_eq_doubleCoset_finiteIdeleStabilizer 17 below · cited by 2 · depth 22
• Strong approximation at v from connectedness of the class-set graph QuaternionAlgebra.exists_eq_finiteIdeleDiagonal_mul_mul_of_forall_classSet_eq_empty_or_eq_univ 33 below · cited by 1 · depth 23
• Finiteness of embedding data in a definite quaternion lattice QuaternionAlgebra.finite_embeddingDatum 0 below · cited by 1 · depth 23
• Reduction of a maximal quaternion order modulo ℓ QuaternionAlgebra.exists_linearMap_matrix_zmod_of_isMaximalOrder_of_ne 13 below · cited by 24 · depth 25
• A Λ-action killed by ℓ descends to M₂(𝔽_ℓ) QuaternionAlgebra.exists_module_matrix_zmod_smul_eq_of_linearMap 0 below · cited by 4 · depth 25
• Right multiplication by c is onto L₀ modulo ℓΛ QuaternionAlgebra.exists_eq_mul_add_smul_of_forall_mul_mem 0 below · cited by 1 · depth 27
• Automorphy of quaternionic period lattices under ι(x) QuaternionAlgebra.denom_smul_qmPeriodMap_smul_eq_and_denom_smul_qmPeriodLattice_smul_eq 0 below · cited by 9 · depth 28
• Determinant of a real matrix representation equals the reduced norm QuaternionAlgebra.det_eq_nrd_of_injective 0 below · cited by 11 · depth 28
• Special integral embedding of B into M₂(H') with centraliser QuaternionAlgebra.exists_algHom_matrix_apply_mem_and_trace_and_forall_iff_mem_range_of_isIndefiniteRamifiedExactlyAt 85 below · cited by 1 · depth 28
• Conjugators agreeing up to powers of r differ by a scalar QuaternionAlgebra.exists_eq_units_map_mul_and_forall_conj_eq_of_forall_exists_zpow_smul_conj_eq_of_awayUnits 29 below · cited by 1 · depth 28
• Homothetic quaternionic period lattices come from a unit QuaternionAlgebra.exists_isUnitOf_smul_eq_of_smul_qmPeriodLattice_eq 0 below · cited by 2 · depth 28
• Maximal order reduces mod N onto M₂(ℤ/N) QuaternionAlgebra.exists_linearMap_matrix_zmod_of_isMaximalOrder_of_not_dvd 17 below · cited by 7 · depth 28
• Maximal order modulo ℓ^m is M₂(ℤ/ℓ^m) QuaternionAlgebra.exists_linearMap_matrix_zmod_pow_of_isMaximalOrder_of_ne 13 below · cited by 1 · depth 28
• An ℓ-torsion Λ-action factors through M₂(𝔽_ℓ) QuaternionAlgebra.exists_module_matrix_zmod_of_smul_eq_zero_of_linearMap 0 below · cited by 1 · depth 28
• Hasse–Schilling norm theorem for a definite rational quaternion algebra QuaternionAlgebra.exists_nrd_eq_of_pos_of_isDefiniteRamifiedExactlyAt 8 below · cited by 1 · depth 28
• Uniformiser and integral basis of a local quaternion division algebra QuaternionAlgebra.exists_sq_eq_natCast_and_setOf_norm_nrd_le_one_eq_of_forall_isUnit_padic 0 below · cited by 1 · depth 28
• Pulling the level identity back along the period map QuaternionAlgebra.forall_qmPeriodLattice_levelIdentity_iff_forall_levelIdentity 0 below · cited by 2 · depth 28
• Recognising H[ℚ,t,s] from an anticommuting spanning pair QuaternionAlgebra.exists_algEquiv_apply_eq_of_mul_self_eq_of_anticommute_of_forall_exists 0 below · cited by 1 · depth 29
• Conjugating an integral embedding into a special one QuaternionAlgebra.exists_algHom_matrix_apply_mem_and_trace_of_apply_mem_of_isIndefiniteRamifiedExactlyAt 69 below · cited by 2 · depth 29
• Commutant of an embedded quaternion pair is the symbol algebra (t,sc') QuaternionAlgebra.exists_algHom_matrix_forall_commute_iff_mem_range_of_mul_self_of_anticommute 0 below · cited by 1 · depth 29
• Embedding B into M₂(H') via a common quadratic subfield QuaternionAlgebra.exists_algHom_matrix_injective_apply_eq_of_isDefiniteRamifiedExactlyAt_of_forall_isUnit_of_pos 7 below · cited by 1 · depth 29
• Scalar commutant of the away-from-r units in M₂(K₀) QuaternionAlgebra.exists_eq_smul_one_of_forall_mem_awayUnits_commute 28 below · cited by 1 · depth 29
• Reduction of a definite maximal order mod N is M₂(ℤ/N) QuaternionAlgebra.exists_linearMap_matrix_zmod_of_isMaximalOrder_of_isDefiniteRamifiedExactlyAt_of_not_dvd 16 below · cited by 1 · depth 29
• Conjugating an embedded order into M₂(𝒪) QuaternionAlgebra.exists_mul_mul_eq_one_and_forall_apply_mem_of_algHom_matrix_injective_of_isOrder_of_isMaximalOrder 57 below · cited by 1 · depth 29
• An anticommuting square root completing a standard quaternion basis QuaternionAlgebra.exists_mul_self_eq_and_anticommute_and_forall_exists_of_mul_self_eq_of_neg_of_neg 0 below · cited by 1 · depth 29
• No multiplicative positive form on an indefinite rational quaternion algebra QuaternionAlgebra.exists_ne_zero_and_not_isUnit_of_forall_map_mul_of_forall_pos 0 below · cited by 1 · depth 29
• Reduced norms of the definite algebra ramified at 2 QuaternionAlgebra.exists_nrd_eq_of_pos_of_isDefiniteRamifiedExactlyAt_two 6 below · cited by 4 · depth 29
• Local conjugacy of the commutant order away from r QuaternionAlgebra.exists_units_forall_mem_localBox_iff_of_forall_iff_mem_range_of_isMaximalOrder 30 below · cited by 1 · depth 29
• Invariance of the local division-algebra condition under isomorphism QuaternionAlgebra.forall_tensorProduct_adicCompletion_isUnit_iff_of_algEquiv 0 below · cited by 1 · depth 29
• Multiplicativity in the second slot of the ramification data QuaternionAlgebra.isDefiniteRamifiedExactlyAt_mul_of_isIndefiniteRamifiedExactlyAt_of_isDefiniteRamifiedExactlyAt 10 below · cited by 1 · depth 29
• Uniqueness of definite rational quaternion algebras ramified exactly at q QuaternionAlgebra.nonempty_algEquiv_of_isDefiniteRamifiedExactlyAt 11 below · cited by 1 · depth 29
• Index of a right translate of a quaternion lattice is nrd² QuaternionAlgebra.relIndex_span_mul_eq_sq_of_nrd_eq 0 below · cited by 4 · depth 29
• Propagating a period-lattice identity across a parameter set QuaternionAlgebra.smul_eq_qmPeriodLattice_of_forall_mem_iff_of_smul_eq_qmPeriodMap 0 below · cited by 2 · depth 29
• Maximal order of a definite quaternion algebra modulo ℓ^m QuaternionAlgebra.exists_linearMap_matrix_zmod_pow_of_isMaximalOrder_of_isDefiniteRamifiedExactlyAt_of_ne 12 below · cited by 1 · depth 30
• r-integrality of a quaternion with Hecke-integral finite idele QuaternionAlgebra.exists_pow_smul_mem_of_finiteAdeleEvalAt_eq_tmul_of_mul_inv_mem_primeHeckeSet 6 below · cited by 2 · depth 30
• Local conjugacy of the commutant order to a maximal order QuaternionAlgebra.exists_units_forall_mem_localBox_iff_of_forall_iff_mem_range_of_isMaximalOrder_of_notMem_of_notMem 20 below · cited by 1 · depth 30
• Local box at ̄ r of the centraliser order QuaternionAlgebra.localBox_eq_localBox_of_forall_iff_mem_range_of_isMaximalOrder_of_mem_asIdeal 22 below · cited by 1 · depth 30
• Skolem–Noether for ℚ-embeddings of a quaternion algebra into M₂(K) QuaternionAlgebra.exists_generalLinearGroup_forall_algHom_apply_eq_conj_algHom_apply 1 below · cited by 2 · depth 31
• Unital injective square-preserving linear maps preserve the reduced norm QuaternionAlgebra.nrd_apply_eq_nrd_of_map_one_of_map_mul_self_of_injective 0 below · cited by 1 · depth 31
• Reduced norm equals determinant under any scalar-fixing splitting QuaternionAlgebra.nrd_eq_det_of_ringEquiv 0 below · cited by 1 · depth 31
• Centralizer of a non-central quaternion is ℚ⟨ 1,α⟩ QuaternionAlgebra.commute_iff_exists_eq_smul_one_add_smul 0 below · cited by 1 · depth 32
• Integral embedding of a quaternion order into M₂(ℤ[ω]) QuaternionAlgebra.exists_algHom_matrix_injective_apply_mem_span_and_trace_of_mul_self_eq_neg_three 0 below · cited by 1 · depth 32
• Special integral embedding of a maximal order into M₂(𝒪) QuaternionAlgebra.exists_algHom_matrix_apply_mem_and_trace_of_isMaximalOrder_of_isDefiniteRamifiedExactlyAt 73 below · cited by 1 · depth 35
• Injective embedding of an order into M₂(𝒪) QuaternionAlgebra.exists_algHom_matrix_injective_forall_apply_mem_of_isOrder_of_isMaximalOrder 61 below · cited by 1 · depth 36
• Quaternion algebra nonsplit at q embeds into M₂(H) QuaternionAlgebra.exists_algHom_matrix_injective_of_isDefiniteRamifiedExactlyAt_of_forall_isUnit 7 below · cited by 1 · depth 37
• Twisted conjugation by t with t²=-c is an involution QuaternionAlgebra.involutive_of_mul_self_eq_neg_smul_of_forall_mul_eq_star_mul 0 below · cited by 3 · depth 37

QuaternionAlgebra.IsDefiniteRamifiedExactlyAt 2

• Splitting of a definite quaternion algebra at a place above r ≠ q QuaternionAlgebra.IsDefiniteRamifiedExactlyAt.exists_algHom_matrix_ratClosure_injective 5 below · cited by 1 · depth 20
• Positive rationals are reduced norms on a definite quaternion algebra QuaternionAlgebra.IsDefiniteRamifiedExactlyAt.exists_nrd_eq_of_pos 6 below · cited by 9 · depth 21

QuaternionAlgebra.IsEichlerOrder 50

• Atkin–Lehner idèle raising an Eichler order to level Nq QuaternionAlgebra.IsEichlerOrder.exists_finiteIdele_meetOrder_isEichlerOrder_mul_of_not_dvd 30 below · cited by 2 · depth 15
• Prescribing one maximal over-order of a squarefree-level Eichler order QuaternionAlgebra.IsEichlerOrder.exists_isMaximalOrder_eq_inf_relIndex_eq_of_squarefree 34 below · cited by 6 · depth 16
• Local Atkin–Lehner element at a prime not dividing the level QuaternionAlgebra.IsEichlerOrder.exists_units_localBox_atkinLehner_of_prime_of_not_dvd 17 below · cited by 5 · depth 16
• Local equality at q ∤ N of an Eichler order and a maximal order above it QuaternionAlgebra.IsEichlerOrder.localBox_eq_localBox_of_isMaximalOrder_of_le_of_not_dvd 17 below · cited by 15 · depth 16
• Eichler level is coprime to the ramified prime QuaternionAlgebra.IsEichlerOrder.not_dvd_of_isDefiniteRamifiedExactlyAt 10 below · cited by 2 · depth 16
• At a ramified prime the Hecke set is one coset QuaternionAlgebra.IsEichlerOrder.exists_primeHeckeSet_eq_setOf_mul_of_isDefiniteRamifiedExactlyAt 17 below · cited by 2 · depth 17
• Local splitting of an Eichler order away from its level QuaternionAlgebra.IsEichlerOrder.exists_ringEquiv_mem_localBox_iff_of_notMem 11 below · cited by 27 · depth 17
• Eichler level independent of the ambient maximal order QuaternionAlgebra.IsEichlerOrder.relIndex_eq_of_isMaximalOrder_of_le 23 below · cited by 4 · depth 17
• Hecke set at the ramified prime is a single coset QuaternionAlgebra.IsEichlerOrder.primeHeckeSet_eq_and_heckeKernel_eq_of_ramified 18 below · cited by 5 · depth 20
• Atkin–Lehner idele at a ramified prime: involutive class-set shift QuaternionAlgebra.IsEichlerOrder.exists_finiteIdele_primeHeckeSet_ramified_conjByFiniteIdele_eq_classSetShift_involutive 23 below · cited by 1 · depth 21
• Reduced norms of Eichler-order ideles realise all unit ideles QuaternionAlgebra.IsEichlerOrder.exists_mem_finiteIdeleStabilizer_forall_nrd_eq 29 below · cited by 11 · depth 21
• Strong approximation for Eichler orders away from a split place QuaternionAlgebra.IsEichlerOrder.exists_eq_finiteIdeleDiagonal_mul_mul 3,748 below · cited by 1 · depth 22
• Strong approximation for Eichler orders away from one prime QuaternionAlgebra.IsEichlerOrder.exists_eq_finiteIdeleDiagonal_mul_mul_of_squarefree_of_not_dvd 3,737 below · cited by 2 · depth 22
• Local Hecke set at a split prime has q+1 classes QuaternionAlgebra.IsEichlerOrder.natCard_setOf_exists_quotientMk_stabilizer_localBox_eq_eq_succ 12 below · cited by 2 · depth 22
• Local U_ℓ set: ℓ cosets and one-sided indices ℓ QuaternionAlgebra.IsEichlerOrder.natCard_setOf_exists_quotientMk_stabilizer_localBox_levelU_eq_of_dvd_of_squarefree 49 below · cited by 2 · depth 22
• Raising the level of an Eichler order by one split prime QuaternionAlgebra.IsEichlerOrder.exists_finiteIdele_meetOrder_isEichlerOrder_mul_of_not_dvd_of_isIndefiniteRamifiedExactlyAt 30 below · cited by 1 · depth 27
• Level module attached to an Eichler order in a maximal order QuaternionAlgebra.IsEichlerOrder.exists_levelModule 37 below · cited by 8 · depth 27
• Normalising a Λ-stable lattice pair as quaternionic period lattices QuaternionAlgebra.IsEichlerOrder.exists_smul_eq_qmPeriodLattice_pair_of_forall_mulVec_mem 60 below · cited by 6 · depth 27
• Homothety of paired QM period lattices versus Fuchsian orbits QuaternionAlgebra.IsEichlerOrder.exists_smul_qmPeriodLattice_pair_eq_iff_exists_fuchsianGroup_smul_eq 9 below · cited by 4 · depth 27
• Right R-stability versus level modules for quaternionic period lattices QuaternionAlgebra.IsEichlerOrder.forall_mem_imp_mem_iff_exists_levelModule_qmPeriodLattice_eq 31 below · cited by 9 · depth 27
• Uniqueness of the level module of an Eichler order QuaternionAlgebra.IsEichlerOrder.levelModule_unique 18 below · cited by 8 · depth 27
• Type number one for Eichler orders over ℤ[1/r] QuaternionAlgebra.IsEichlerOrder.exists_conjByFiniteIdele_finiteIdeleDiagonal_mul_eq_of_squarefree_of_not_dvd_of_ne 61 below · cited by 1 · depth 28
• Two periods of a levelled lattice pair lie in one Fuchsian orbit QuaternionAlgebra.IsEichlerOrder.exists_fuchsianGroup_smul_eq_of_smul_eq_qmPeriodLattice_of_forall_mem_imp_mem 41 below · cited by 4 · depth 28
• Squarefree Eichler orders as intersections with any containing maximal order QuaternionAlgebra.IsEichlerOrder.exists_isMaximalOrder_and_eq_inf_and_relIndex_eq_of_squarefree_of_le 34 below · cited by 2 · depth 28
• Unit ideles are reduced norms from an Eichler order QuaternionAlgebra.IsEichlerOrder.exists_mem_finiteIdeleStabilizer_forall_nrd_eq_of_isDefiniteRamifiedExactlyAt 32 below · cited by 1 · depth 28
• Norm-ℓ elements of an Eichler order meet its prime Hecke set QuaternionAlgebra.IsEichlerOrder.exists_mem_primeHeckeSet_coe_eq_tmul_one_of_nrd_eq 4 below · cited by 2 · depth 28
• Norm-r elements of an Eichler order at a ramified prime QuaternionAlgebra.IsEichlerOrder.exists_nrd_eq_and_forall_exists_isUnitOf_mul_eq_of_isIndefiniteRamifiedExactlyAt 55 below · cited by 1 · depth 28
• Transversal norm-ℓ elements of an Eichler order, up to norm-one units QuaternionAlgebra.IsEichlerOrder.exists_nrd_eq_levelIdentity_and_forall_exists_isUnitOf_nrd_eq_one_mul_mul_iff_of_levelIdentity 62 below · cited by 1 · depth 28
• Γ-stability of uniformised periods with R-level structure QuaternionAlgebra.IsEichlerOrder.exists_smul_eq_qmPeriodLattice_smul_and_forall_mem_imp_mem_of_mem_fuchsianGroup 1 below · cited by 4 · depth 28
• Atkin–Lehner unit and the level-N Hecke criterion QuaternionAlgebra.IsEichlerOrder.exists_units_atkinLehner_qmPeriodLattice_levelModule_iff_exists_mem_levelHeckeUSet 87 below · cited by 1 · depth 28
• Local Atkin–Lehner element for an Eichler order at ℓ QuaternionAlgebra.IsEichlerOrder.exists_units_localBox_atkinLehner_of_isIndefiniteRamifiedExactlyAt_of_not_dvd 17 below · cited by 1 · depth 28
• Norm-ℓ elements of an Eichler order and period sublattices QuaternionAlgebra.IsEichlerOrder.forall_le_qmPeriodLattice_transversal_iff_exists_mem_nrd_eq 61 below · cited by 3 · depth 28
• Eichler order locally maximal away from its level QuaternionAlgebra.IsEichlerOrder.localBox_eq_localBox_of_isMaximalOrder_of_le_of_isIndefiniteRamifiedExactlyAt_of_not_dvd 17 below · cited by 1 · depth 28
• Index of an Eichler order in any containing maximal order QuaternionAlgebra.IsEichlerOrder.relIndex_eq_of_isMaximalOrder_of_le_of_ne_zero 23 below · cited by 2 · depth 28
• Eichler orders of squarefree level form one genus QuaternionAlgebra.IsEichlerOrder.exists_conjByFiniteIdele_eq_and_conjByFiniteIdele_eq_of_squarefree 38 below · cited by 1 · depth 29
• Strong approximation away from a split place, Eichler order QuaternionAlgebra.IsEichlerOrder.exists_eq_finiteIdeleDiagonal_mul_mul_of_ne 44 below · cited by 1 · depth 29
• Unit reduced norms of Eichler orders at discriminant 2 QuaternionAlgebra.IsEichlerOrder.exists_mem_finiteIdeleStabilizer_forall_nrd_eq_of_isDefiniteRamifiedExactlyAt_two 29 below · cited by 3 · depth 29
• Prescribed reduced norms at the split places of an Eichler order QuaternionAlgebra.IsEichlerOrder.exists_mem_finiteIdeleStabilizer_forall_nrd_eq_of_not_forall_isUnit 18 below · cited by 1 · depth 29
• Transversal index-ℓ² ideals come from norm-ℓ elements QuaternionAlgebra.IsEichlerOrder.exists_mem_nrd_eq_forall_mem_iff_mul_of_relIndex_eq_sq_of_transversal 56 below · cited by 2 · depth 29
• Mod-ℓ unipotent element of Λ carrying Λ t to Λ t' QuaternionAlgebra.IsEichlerOrder.exists_nrd_eq_one_add_and_forall_smul_mul_eq_and_forall_mul_mul_eq_of_levelIdentity 19 below · cited by 1 · depth 29
• Fuchsian translates of period data with Eichler level and generator QuaternionAlgebra.IsEichlerOrder.exists_smul_eq_qmPeriodLattice_smul_and_smul_eq_qmPeriodMap_mul_of_mem_fuchsianGroup 1 below · cited by 1 · depth 29
• Global Atkin–Lehner element of reduced norm N QuaternionAlgebra.IsEichlerOrder.exists_units_mem_nrd_eq_level_forall_mem_iff_conj_mem 74 below · cited by 1 · depth 29
• Level identity at ℓ ∣ N versus idelic Hecke membership of wtw⁻¹ QuaternionAlgebra.IsEichlerOrder.levelIdentity_iff_exists_mem_levelHeckeUSet_conj_of_dvd 24 below · cited by 1 · depth 29
• Level identity ℓ J' + Λ t = J't for ℓ ∤ N QuaternionAlgebra.IsEichlerOrder.levelIdentity_of_not_dvd 2 below · cited by 1 · depth 29
• Diagonal idele in the level Hecke set QuaternionAlgebra.IsEichlerOrder.exists_mem_levelHeckeUSet_coe_eq_tmul_iff 3 below · cited by 1 · depth 30
• Level identity at ℓ ∣ N via conjugation criterion QuaternionAlgebra.IsEichlerOrder.levelIdentity_iff_not_conj_eq_and_not_conj_le_of_dvd 22 below · cited by 1 · depth 30
• Norm-ℓ conjugation flip between twin maximal orders QuaternionAlgebra.IsEichlerOrder.exists_mem_forall_pow_smul_star_mul_mul_ne_smul_of_forall_pow_smul_mul_mul_star_ne_smul_of_inf_eq_of_dvd 35 below · cited by 1 · depth 31
• Flip: s⁻¹R₁s⊆Λ₁[1/r] when sR₁s⁻¹ fails QuaternionAlgebra.IsEichlerOrder.forall_exists_pow_smul_star_mul_mul_eq_smul_of_forall_pow_smul_mul_mul_star_ne_smul_of_inf_eq_of_dvd 36 below · cited by 1 · depth 31
• Transversality of a norm-ℓ element at ℓ ∣ N QuaternionAlgebra.IsEichlerOrder.forall_mul_star_mem_imp_mem_iff_not_conj_eq_and_not_conj_le_of_dvd 16 below · cited by 1 · depth 31
• Level identity for a norm-ℓ element versus transversality QuaternionAlgebra.IsEichlerOrder.levelIdentity_iff_forall_mul_star_mem_imp_mem 8 below · cited by 1 · depth 31

QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt 8

• Real splitting: indefinite rational quaternion algebra embeds in M₂(ℝ) QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt.exists_algHom_matrix_injective 1 below · cited by 4 · depth 26
• A quaternion algebra ramified at a finite place is a division algebra QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt.isUnit_of_ne_zero 0 below · cited by 46 · depth 26
• Every non-zero rational is a reduced norm (indefinite case) QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt.exists_nrd_eq 6 below · cited by 4 · depth 28
• Choice of auxiliary prime ℓ ∈ {q,q'} invertible in a local ring QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt.exists_prime_isUnit_natCast_forall_isUnit_tensorProduct_padic 2 below · cited by 1 · depth 31
• Square root of -3 in the discriminant-6 quaternion algebra QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt.exists_mul_self_eq_neg_three 6 below · cited by 1 · depth 32
• Division condition for H⊗mathbb Q_ℓ at rational primes QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt.forall_isUnit_tensorProduct_padic_iff 0 below · cited by 1 · depth 32
• Complexified image of a maximal order spans M₂(ℂ) QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt.span_range_map_algebraMap_eq_top_of_isMaximalOrder 1 below · cited by 1 · depth 32
• Symmetry of `IsIndefiniteRamifiedExactlyAt` in its two levels QuaternionAlgebra.IsIndefiniteRamifiedExactlyAt.symm 0 below · cited by 1 · depth 39

QuaternionAlgebra.IsMaximalOrder 92

• Conjugating a maximal quaternion order by a finite idele QuaternionAlgebra.IsMaximalOrder.conjByFiniteIdele 4 below · cited by 17 · depth 16
• Existence of Eichler orders of level N inside a maximal order QuaternionAlgebra.IsMaximalOrder.exists_le_isEichlerOrder_of_isDefiniteRamifiedExactlyAt 26 below · cited by 1 · depth 16
• Maximal orders in a definite quaternion algebra over ℚ are adelically conjugate QuaternionAlgebra.IsMaximalOrder.exists_conjByFiniteIdele_eq_of_isDefiniteRamifiedExactlyAt 25 below · cited by 1 · depth 17
• Eichler orders of level N inside a maximal order QuaternionAlgebra.IsMaximalOrder.exists_le_isEichlerOrder_of_forall_not_forall_isUnit 26 below · cited by 1 · depth 17
• Local box of a maximal order is a conjugate of M₂(ℤᵥ) QuaternionAlgebra.IsMaximalOrder.exists_localBox_iff_generalLinearGroup_conj_mem_adicCompletionIntegers 7 below · cited by 20 · depth 17
• Two maximal quaternion orders simultaneously standard at a split place QuaternionAlgebra.IsMaximalOrder.exists_pair_localBox_iff_conj_diagonal_pow_mem_adicCompletionIntegers 9 below · cited by 12 · depth 17
• Maximal orders agree locally at a division place QuaternionAlgebra.IsMaximalOrder.localBox_eq_localBox_of_forall_isUnit 7 below · cited by 24 · depth 17
• Local box of a maximal order is locally maximal QuaternionAlgebra.IsMaximalOrder.localBox_eq_of_le_of_forall_mem_localBox_iff_generalLinearGroup_conj 3 below · cited by 1 · depth 17
• Ramified-prime Hecke idele: its lattice and commutation with the level QuaternionAlgebra.IsMaximalOrder.mem_ofFiniteIdele_iff_and_ofFiniteIdele_mul_mul_eq_of_mem_primeHeckeSet_of_finiteAdeleEvalAt_eq_one 13 below · cited by 1 · depth 17
• Right ideals of a maximal order arise from finite ideles QuaternionAlgebra.IsMaximalOrder.exists_ofFiniteIdele_eq_of_forall_mul_mem 21 below · cited by 3 · depth 18
• Local type of a normalised connecting finite idele QuaternionAlgebra.IsMaximalOrder.localBoxUnits_and_exists_eq_mul_diagonal_mul_of_relIndex_inf_conjByFiniteIdele_eq 31 below · cited by 11 · depth 18
• Algebra isomorphisms carry maximal orders to maximal orders QuaternionAlgebra.IsMaximalOrder.map_algEquiv 0 below · cited by 1 · depth 18
• Local maximal order is the reduced-norm valuation ring QuaternionAlgebra.IsMaximalOrder.mem_localBox_iff_nrd_mem_adicCompletionIntegers_of_forall_isUnit 6 below · cited by 24 · depth 18
• Maximal orders force a ≠ 0 and b ≠ 0 QuaternionAlgebra.IsMaximalOrder.ne_zero_and_ne_zero 0 below · cited by 12 · depth 18
• Shifting locally principal ideals by the ramified prime P QuaternionAlgebra.IsMaximalOrder.ofFiniteIdele_mul_eq_mul_and_mem_ofFiniteIdele_mul_mul_iff_of_isDefiniteRamifiedExactlyAt 12 below · cited by 1 · depth 18
• Full right Λ-sublattices of locally principal ideals remain locally principal QuaternionAlgebra.IsMaximalOrder.exists_eq_ofFiniteIdele_of_forall_mul_mem 23 below · cited by 2 · depth 19
• A uniformiser of reduced norm valuation one in a maximal order QuaternionAlgebra.IsMaximalOrder.exists_mem_padicValRat_nrd_eq_one_of_isDefiniteRamifiedExactlyAt 11 below · cited by 2 · depth 19
• Integral right ideals split off a power of the ramified prime QuaternionAlgebra.IsMaximalOrder.exists_ofFiniteIdele_eq_inf_setOf_le_padicValRat_nrd 14 below · cited by 1 · depth 19
• Local principality at a ramified place of a right ideal QuaternionAlgebra.IsMaximalOrder.exists_units_forall_mem_localBox_iff_of_mem_asIdeal 8 below · cited by 1 · depth 19
• Divisibility by q' in a maximal order ramified at q' QuaternionAlgebra.IsMaximalOrder.exists_eq_natCast_smul_of_two_le_padicValRat_nrd 8 below · cited by 2 · depth 21
• Maximal order at a division place is the nrd valuation ring QuaternionAlgebra.IsMaximalOrder.exists_ringEquiv_coe_localBox_eq_setOf_norm_nrd_le_one_of_forall_isUnit 7 below · cited by 4 · depth 22
• Local over-orders of an Iwahori order: only two QuaternionAlgebra.IsMaximalOrder.localBox_eq_or_localBox_eq_of_inf_le_of_localBox_iff_conj_diagonal 9 below · cited by 1 · depth 23
• mathfrak Pᵣ²⊆ rΛ for maximal orders, indefinite ramified case QuaternionAlgebra.IsMaximalOrder.exists_mul_eq_natCast_smul_of_dvd_nrd_of_dvd_nrd_of_isIndefiniteRamifiedExactlyAt 12 below · cited by 8 · depth 24
• Index of Λ-stable subgroups between ℓΛ and Λ QuaternionAlgebra.IsMaximalOrder.relIndex_leftIdeal_mem_of_ne_of_ne 14 below · cited by 5 · depth 24
• Freeness of rank one over Λ/rΛ for faithful r⁴-modules QuaternionAlgebra.IsMaximalOrder.exists_generator_of_natCard_eq_pow_four_of_isIndefiniteRamifiedExactlyAt 16 below · cited by 1 · depth 25
• Left ideal of index ℓ² in a maximal quaternion order QuaternionAlgebra.IsMaximalOrder.exists_submodule_le_mul_mem_relIndex_eq_sq 29 below · cited by 7 · depth 25
• Line images in a rank-one Λ/ℓΛ-module QuaternionAlgebra.IsMaximalOrder.lineImage_classification 16 below · cited by 1 · depth 25
• The ℓ+1 proper Λ-lines mod ℓ and their intersections QuaternionAlgebra.IsMaximalOrder.natCard_properLine_eq_and_inf_eq 15 below · cited by 4 · depth 25
• Square of the ramified prime of a maximal order is rΛ QuaternionAlgebra.IsMaximalOrder.span_mul_ramifiedPrime_eq_of_isIndefiniteRamifiedExactlyAt 14 below · cited by 4 · depth 25
• Reduced norm divisible by r² forces h ∈ rΛ QuaternionAlgebra.IsMaximalOrder.exists_eq_natCast_smul_of_two_le_padicValRat_nrd_of_isIndefiniteRamifiedExactlyAt 12 below · cited by 3 · depth 26
• Principal two-sided generator at a ramified prime QuaternionAlgebra.IsMaximalOrder.exists_generator_ramifiedPrime_of_isIndefiniteRamifiedExactlyAt 49 below · cited by 8 · depth 26
• Eichler orders of squarefree level inside a maximal order QuaternionAlgebra.IsMaximalOrder.exists_le_isEichlerOrder_of_isIndefiniteRamifiedExactlyAt_of_squarefree 31 below · cited by 3 · depth 26
• Maximal order has element with nrd exactly divisible by r QuaternionAlgebra.IsMaximalOrder.exists_mem_dvd_nrd_not_sq_dvd_nrd_of_isIndefiniteRamifiedExactlyAt 13 below · cited by 2 · depth 26
• Local splitting carrying a maximal order to integral matrices QuaternionAlgebra.IsMaximalOrder.exists_ringEquiv_mem_localBox_iff_of_isIndefiniteRamifiedExactlyAt_of_prime 12 below · cited by 6 · depth 26
• Left ideals between rΛ and a maximal order at a ramified prime QuaternionAlgebra.IsMaximalOrder.leftIdeal_eq_or_eq_or_eq_of_isIndefiniteRamifiedExactlyAt_of_eq_or_eq 14 below · cited by 14 · depth 26
• A maximal order in H[ℚ,a,b] is free of rank four QuaternionAlgebra.IsMaximalOrder.exists_forall_existsUnique_eq_sum_zsmul 0 below · cited by 2 · depth 27
• Reduced norm ± r attained in a maximal order QuaternionAlgebra.IsMaximalOrder.exists_mem_nrd_eq_or_eq_neg_of_isIndefiniteRamifiedExactlyAt 41 below · cited by 2 · depth 27
• Transitivity on Λ-lines mod m, including ramified ℓ QuaternionAlgebra.IsMaximalOrder.exists_mul_mem_line_of_line_of_prime 25 below · cited by 2 · depth 27
• A left generator of the ramified prime normalises a maximal order QuaternionAlgebra.IsMaximalOrder.forall_exists_mul_eq_mul_of_forall_dvd_nrd_iff_of_isIndefiniteRamifiedExactlyAt 15 below · cited by 1 · depth 27
• Exactly ℓ stable lifts of a level-N subgroup QuaternionAlgebra.IsMaximalOrder.natCard_levelLift_eq_of_dvd 16 below · cited by 1 · depth 27
• Left ideals of an indefinite maximal order are principal QuaternionAlgebra.IsMaximalOrder.exists_eq_map_mulRight_of_isIndefiniteRamifiedExactlyAt 44 below · cited by 4 · depth 28
• Norm-one units of a maximal order move level-N modules transitively QuaternionAlgebra.IsMaximalOrder.exists_isUnitOf_nrd_eq_one_forall_mem_iff_exists_mul_of_levelModule 35 below · cited by 3 · depth 28
• Maximal order modulo ℓ: split or ramified alternative QuaternionAlgebra.IsMaximalOrder.exists_linearMap_matrix_zmod_or_forall_eq_or_eq_or_eq_of_prime 23 below · cited by 1 · depth 28
• Finite idèle units of a maximal order with prescribed reduced norms QuaternionAlgebra.IsMaximalOrder.exists_mem_finiteIdeleStabilizer_forall_nrd_eq_of_isIndefiniteRamifiedExactlyAt 27 below · cited by 3 · depth 28
• Element of a maximal order irreducible modulo a ramified prime QuaternionAlgebra.IsMaximalOrder.exists_mem_trd_eq_nrd_eq_forall_sq_sub_mul_add_ne_zero_of_isIndefiniteRamifiedExactlyAt 16 below · cited by 3 · depth 28
• Transitivity of right multiplication on Λ-lines modulo ℓ QuaternionAlgebra.IsMaximalOrder.exists_mul_mem_line_of_line 14 below · cited by 1 · depth 28
• Lattices with quaternionic multiplication are homothetic to period lattices QuaternionAlgebra.IsMaximalOrder.exists_smul_eq_qmPeriodLattice_of_forall_mulVec_mem 49 below · cited by 2 · depth 28
• Indices attached to two maximal orders in a rational quaternion algebra QuaternionAlgebra.IsMaximalOrder.relIndex_inf_eq_and_relIndex_mul_eq_sq 26 below · cited by 1 · depth 28
• Trace of a maximal order acting on a plane QuaternionAlgebra.IsMaximalOrder.trace_eq_intCast_of_add_star_eq_of_finrank_eq_two 15 below · cited by 3 · depth 28
• Filtration of a finite Λ-stable subgroup with square steps QuaternionAlgebra.IsMaximalOrder.exists_chain_subgroup_relIndex_eq_sq 30 below · cited by 2 · depth 29
• Holomorphic normalisation of a Λ-stable lattice frame in ℂ² QuaternionAlgebra.IsMaximalOrder.exists_differentiableOn_smul_span_eq_qmPeriodLattice_of_latticeFrame 0 below · cited by 2 · depth 29
• Divisibility by p in a maximal order at a ramified prime QuaternionAlgebra.IsMaximalOrder.exists_eq_natCast_smul_of_two_le_padicValRat_nrd_of_forall_isUnit 11 below · cited by 1 · depth 29
• Orienting quaternionic period lattices from the lower half-plane QuaternionAlgebra.IsMaximalOrder.exists_forall_exists_mulVec_eq_iff_smul_mem_qmPeriodLattice_of_im_neg 42 below · cited by 1 · depth 29
• Lattices with quaternionic multiplication, maximal order case QuaternionAlgebra.IsMaximalOrder.exists_im_ne_zero_forall_mem_smul_iff_of_forall_mulVec_mem 45 below · cited by 1 · depth 29
• Norm-one unit congruent mod N to a given element of a maximal order QuaternionAlgebra.IsMaximalOrder.exists_isUnitOf_nrd_eq_one_sub_mem_of_nrd_eq 30 below · cited by 2 · depth 29
• Maximal orders contain an element of reduced norm valuation one QuaternionAlgebra.IsMaximalOrder.exists_mem_padicValRat_nrd_eq_one_of_forall_isUnit 11 below · cited by 1 · depth 29
• Norm-r elements in a maximal order at a ramified prime QuaternionAlgebra.IsMaximalOrder.exists_nrd_eq_and_forall_exists_isUnitOf_mul_eq_of_isIndefiniteRamifiedExactlyAt 47 below · cited by 2 · depth 29
• Matching level-N modules by an element of norm ≡ 1 QuaternionAlgebra.IsMaximalOrder.exists_nrd_eq_forall_mul_mem_of_levelModule 17 below · cited by 1 · depth 29
• Right Λ-ideals of full rank arise from finite ideles QuaternionAlgebra.IsMaximalOrder.exists_ofFiniteIdele_eq_of_forall_mul_mem_of_isIndefiniteRamifiedExactlyAt 21 below · cited by 1 · depth 29
• A left Λ-ideal of index ℓ² transversal to a level module QuaternionAlgebra.IsMaximalOrder.exists_submodule_relIndex_eq_sq_and_transversal_of_levelModule 17 below · cited by 1 · depth 29
• Equivariant tensors for a maximal quaternion order form a line QuaternionAlgebra.IsMaximalOrder.finrank_eq_one_of_forall_mem_iff_forall_map_tmul_eq_of_finrank_eq_two 15 below · cited by 2 · depth 29
• Local index of a product of maximal orders is a square QuaternionAlgebra.IsMaximalOrder.relIndex_localBox_mul_eq_sq 23 below · cited by 1 · depth 29
• Maximal orders contain a unit of reduced norm -1 QuaternionAlgebra.IsMaximalOrder.exists_isUnitOf_nrd_eq_neg_one 40 below · cited by 5 · depth 30
• Rank-two right 𝒪-lattices in H² are free QuaternionAlgebra.IsMaximalOrder.exists_matrix_forall_mem_iff_forall_mulVec_mem 56 below · cited by 3 · depth 30
• Norm-one local lift congruent to c modulo N QuaternionAlgebra.IsMaximalOrder.exists_mem_localBox_nrd_eq_one_eq_tmul_add_smul 14 below · cited by 1 · depth 30
• Prime-norm elements of a quaternion order lie in the Hecke set at ℓ QuaternionAlgebra.IsMaximalOrder.exists_mem_primeHeckeSet_coe_eq_tmul_one_of_nrd_eq 4 below · cited by 1 · depth 30
• Left ideals of index ℓ² in indefinite maximal orders are principal QuaternionAlgebra.IsMaximalOrder.exists_nrd_eq_forall_mem_iff_exists_mul_of_relIndex_eq_sq_of_isIndefiniteRamifiedExactlyAt 47 below · cited by 2 · depth 30
• Separability element for S⊗_ℤΛ when qq' is invertible QuaternionAlgebra.IsMaximalOrder.exists_separabilityElement_tensor_of_isIndefiniteRamifiedExactlyAt_of_isUnit 20 below · cited by 1 · depth 30
• Homothetic quaternionic period lattices and Fuchsian orbits QuaternionAlgebra.IsMaximalOrder.exists_smul_qmPeriodLattice_eq_iff_exists_fuchsianGroup_smul_eq_of_level_one 6 below · cited by 1 · depth 30
• Hecke dictionary for quaternionic period lattices QuaternionAlgebra.IsMaximalOrder.forall_le_qmPeriodLattice_iff_exists_mem_of_nrd_eq 63 below · cited by 1 · depth 30
• Bounded left Λ_w-stable subgroups of a local division quaternion algebra are principal QuaternionAlgebra.IsMaximalOrder.exists_isUnit_forall_mem_iff_exists_mem_localBox_eq_mul_of_forall_isUnit 8 below · cited by 1 · depth 31
• Two full right ideals of a maximal quaternion order form a free rank-two module QuaternionAlgebra.IsMaximalOrder.exists_matrix_forall_mulVec_mem_iff_of_le 53 below · cited by 2 · depth 31
• Local 4×4 matrix frame transporting τ, j and the order R QuaternionAlgebra.IsMaximalOrder.exists_ringHom_matrix_prod_forall_mem_localBox_iff_of_algHom_comm_of_notMem 13 below · cited by 2 · depth 31
• Full-rank right ideals of a maximal order are invertible QuaternionAlgebra.IsMaximalOrder.exists_sum_mul_eq_one_of_forall_mul_mem 54 below · cited by 1 · depth 31
• Two ideals at one split place span a free rank-two lattice QuaternionAlgebra.IsMaximalOrder.exists_matrix_forall_mulVec_mem_iff_mem_ofFiniteIdele_of_forall_finiteAdeleEvalAt_eq_one 14 below · cited by 1 · depth 32
• Twin maximal orders at a prime dividing the level QuaternionAlgebra.IsMaximalOrder.exists_ringEquiv_generalLinearGroup_forall_mem_localBox_iff_of_inf_eq_of_dvd_of_squarefree 30 below · cited by 2 · depth 32
• Right 𝒪-ideals represented by ideles supported at one split place QuaternionAlgebra.IsMaximalOrder.exists_units_forall_mem_iff_mem_ofFiniteIdele_of_forall_mul_mem 49 below · cited by 1 · depth 32
• Counting Λ-stable sublattices of index ℓ² in a period lattice QuaternionAlgebra.IsMaximalOrder.natCard_sublattice_qmPeriodLattice_eq_add_one 19 below · cited by 1 · depth 32
• Reduced trace of a plane representation of a maximal order QuaternionAlgebra.IsMaximalOrder.trace_eq_intCast_of_add_star_eq_of_finrank_eq_two_of_charZero 1 below · cited by 3 · depth 33
• Uniqueness of ⋆-alternating forms on a rank-one module QuaternionAlgebra.IsMaximalOrder.exists_generator_of_alternating_starAdjoint_forms 1 below · cited by 2 · depth 37
• Generator of ⋆-alternating forms is a perfect pairing QuaternionAlgebra.IsMaximalOrder.isPerfPair_of_generator_of_alternating_starAdjoint_forms 62 below · cited by 1 · depth 37
• Uniqueness of ⋆-alternating forms up to scalar QuaternionAlgebra.IsMaximalOrder.existsUnique_eq_smul_of_isPerfPair_of_alternating_starAdjoint 2 below · cited by 1 · depth 38
• Maximal order in an indefinite quaternion algebra spans M₂(k) universally QuaternionAlgebra.IsMaximalOrder.exists_linearMap_matrix_span_eq_top_forall_exists_algHom_of_isAlgClosed 14 below · cited by 1 · depth 38
• Residue structure at a ramified prime of a maximal order QuaternionAlgebra.IsMaximalOrder.exists_mem_add_star_eq_and_mul_add_mul_sub_smul_eq_and_star_sub_eq_of_eq_or_eq 61 below · cited by 1 · depth 38
• Biadditive symbol identity for sheaves of modules on a scheme QuaternionAlgebra.IsMaximalOrder.exists_nonempty_iso_foldr_tensor_tensorPow_of_nonempty_iso_tensor 2 below · cited by 1 · depth 38
• Trace-dual of a maximal order equals μ⁻¹Λ QuaternionAlgebra.IsMaximalOrder.forall_exists_intCast_eq_trd_mul_iff_mul_mem_of_isIndefiniteRamifiedExactlyAt 57 below · cited by 2 · depth 38
• The reduced traces of μΛ form qq'ℤ QuaternionAlgebra.IsMaximalOrder.trd_mul_mem_and_exists_trd_mul_eq_of_isIndefiniteRamifiedExactlyAt 58 below · cited by 2 · depth 38
• Trace divisibility modulo a ramified prime forces rmidnrd QuaternionAlgebra.IsMaximalOrder.dvd_nrd_of_forall_dvd_trd_mul_of_isIndefiniteRamifiedExactlyAt 19 below · cited by 2 · depth 39
• At a ramified prime, r ∣ nrd implies r ∣ trd QuaternionAlgebra.IsMaximalOrder.dvd_trd_of_dvd_nrd_of_isIndefiniteRamifiedExactlyAt 50 below · cited by 2 · depth 39
• Non-degeneracy of the trace pairing on Λ/ℓΛ QuaternionAlgebra.IsMaximalOrder.exists_eq_natCast_smul_of_forall_dvd_trd_mul_of_ne_of_ne 15 below · cited by 1 · depth 39
• Divisibility by r from r²-divisible traces against P QuaternionAlgebra.IsMaximalOrder.exists_eq_natCast_smul_of_forall_sq_dvd_trd_mul_of_isIndefiniteRamifiedExactlyAt 53 below · cited by 1 · depth 39
• Casimir identity for the involution x ↦ μ⁻¹x̄μ QuaternionAlgebra.IsMaximalOrder.exists_sum_smul_biadditive_mul_eq_sum_smul_biadditive_mul_star 1 below · cited by 1 · depth 39

QuaternionAlgebra.IsOrder 56

• Commuting class-set Hecke matrices at coprime indices QuaternionAlgebra.IsOrder.commute_classSetHeckeMatrix_of_subset_primeHeckeSet_of_coprime 4 below · cited by 1 · depth 16
• Idelic conjugates of orders in H[ℚ,a,b] are orders QuaternionAlgebra.IsOrder.conjByFiniteIdele 2 below · cited by 70 · depth 16
• A ℤ-basis of a quaternion order is a ℚ-basis QuaternionAlgebra.IsOrder.exists_basis_span_eq 1 below · cited by 35 · depth 16
• Adelic box and stabiliser of an order meeting a conjugate QuaternionAlgebra.IsOrder.finiteAdeleBox_inf_conjByFiniteIdele_eq_and_finiteIdeleStabilizer_le 7 below · cited by 27 · depth 16
• Hecke sets meet only finitely many stabiliser cosets QuaternionAlgebra.IsOrder.finite_setOf_exists_mem_quotientMk_eq_of_subset_primeHeckeSet 1 below · cited by 15 · depth 16
• Idelic stabiliser of an order is detected place by place QuaternionAlgebra.IsOrder.mem_finiteIdeleStabilizer_iff_forall_map_finiteAdeleEvalAt_mem_localBoxUnits 0 below · cited by 79 · depth 16
• Integrality of reduced norm and trace on an order QuaternionAlgebra.IsOrder.exists_intCast_eq_nrd_and_exists_intCast_eq_trd 0 below · cited by 75 · depth 17
• An order in a rational quaternion algebra has ℤ-rank 4 QuaternionAlgebra.IsOrder.finrank_eq_four 0 below · cited by 6 · depth 17
• Adelic Brandt-matrix count for a left-stable Hecke set QuaternionAlgebra.IsOrder.heckeKernel_mk_mk_eq_natCard_of_forall_mul_mem 2 below · cited by 1 · depth 17
• Brandt matrix entry as a count of lattices QuaternionAlgebra.IsOrder.heckeKernel_primeHeckeSet_mk_mk_eq_natCard 2 below · cited by 5 · depth 17
• Conjugation by a finite idele preserves relative index of orders QuaternionAlgebra.IsOrder.relIndex_conjByFiniteIdele 12 below · cited by 1 · depth 17
• One-place enlargement of a quaternion order at a split place QuaternionAlgebra.IsOrder.exists_isOrder_le_localBox_iff_conj_apply_mem_adicCompletionIntegers 2 below · cited by 2 · depth 18
• Lattice criterion for the prime Hecke set at ℓ QuaternionAlgebra.IsOrder.exists_mem_primeHeckeSet_eq_ofFiniteIdele_mul_iff 11 below · cited by 3 · depth 18
• Divisibility of idelic lattices versus integrality of n⁻¹g QuaternionAlgebra.IsOrder.ofFiniteIdele_mul_le_zsmul_ofFiniteIdele_iff_inv_smul_mem_finiteAdeleBox 1 below · cited by 5 · depth 18
• Index of xgΛ̂∩ H as product of local indices QuaternionAlgebra.IsOrder.relIndex_ofFiniteIdele_mul_eq_finprod_relIndex_map_mulLeft_localBox 10 below · cited by 2 · depth 18
• Local index of gΛᵥ in Λᵥ is a power of ℓ QuaternionAlgebra.IsOrder.exists_relIndex_map_mulLeft_localBox_eq_pow 4 below · cited by 1 · depth 19
• One-place idele with local elementary divisors (1,ℓ) is a prime Hecke element QuaternionAlgebra.IsOrder.mem_primeHeckeSet_of_finiteAdeleEvalAt_eq_conj_diagonal 1 below · cited by 1 · depth 19
• Strong approximation away from a split place, double-coset form QuaternionAlgebra.IsOrder.exists_eq_finiteIdeleDiagonal_mul_mul_of_forall_nrd_eq_one 20 below · cited by 3 · depth 21
• Reduced trace and norm of an element of a quaternion order are integral QuaternionAlgebra.IsOrder.exists_int_trd_eq_and_nrd_eq 1 below · cited by 25 · depth 21
• Strong approximation for norm-one quaternions away from a split place QuaternionAlgebra.IsOrder.exists_nrd_eq_one_and_eq_finiteIdeleDiagonal_mul_mul_of_forall_nrd_eq_one 20 below · cited by 9 · depth 21
• Units of definite rational quaternion orders satisfy u¹²=1 QuaternionAlgebra.IsOrder.pow_twelve_eq_one_and_not_dvd_natCard_isUnitOf 3 below · cited by 2 · depth 21
• Kneser reduction: strong approximation away from v in double-coset form QuaternionAlgebra.IsOrder.exists_eq_finiteIdeleDiagonal_mul_mul_of_forall_exists_nrd_eq_one_tmul_eq_add_smul 10 below · cited by 1 · depth 22
• Non-central approximable norm-one element at a place w ≠ v QuaternionAlgebra.IsOrder.exists_ne_neg_one_forall_exists_nrd_eq_one_tmul_eq_add_smul 8 below · cited by 2 · depth 22
• Kneser's reduction of strong approximation, norm-one global factor QuaternionAlgebra.IsOrder.exists_nrd_eq_one_and_eq_finiteIdeleDiagonal_mul_mul_of_forall_exists_nrd_eq_one_tmul_eq_add_smul 10 below · cited by 1 · depth 22
• Finiteness and norm one of units in definite orders QuaternionAlgebra.IsOrder.finite_isUnitOf_and_nrd_eq_one 2 below · cited by 7 · depth 22
• Kneser's normal-subgroup step at a split place QuaternionAlgebra.IsOrder.forall_exists_nrd_eq_one_tmul_eq_add_smul_of_exists_ne_neg_one 8 below · cited by 2 · depth 22
• Units of the conjugated order B∩βwidehatΛβ⁻¹ QuaternionAlgebra.IsOrder.isUnitOf_conjByFiniteIdele_iff 3 below · cited by 2 · depth 22
• Idelic unit index of an order localises at one place QuaternionAlgebra.IsOrder.relIndex_finiteIdeleStabilizer_inf_map_conj_eq_local 5 below · cited by 2 · depth 22
• Uniform denominator for integral quaternions up to conjugacy QuaternionAlgebra.IsOrder.exists_forall_exists_units_smul_conj_mem_of_int_trd_nrd 0 below · cited by 1 · depth 23
• Weak approximation for the norm-one group of a rational quaternion algebra QuaternionAlgebra.IsOrder.exists_nrd_eq_one_forall_tmul_eq_add_smul_of_finset 2 below · cited by 5 · depth 23
• Reduced norm of an order has a nontrivial zero mod p QuaternionAlgebra.IsOrder.exists_mem_dvd_nrd_forall_ne_smul 3 below · cited by 6 · depth 24
• The index of nΛ in a rational quaternion order is n⁴ QuaternionAlgebra.IsOrder.relIndex_span_smul_eq_pow_four 2 below · cited by 31 · depth 24
• Integrality away from v means r-power denominators QuaternionAlgebra.IsOrder.forall_tmul_one_mem_localBox_iff_exists_pow_smul_mem 3 below · cited by 7 · depth 25
• A line L₀ with ℓΛ⊆ L₀⊆Λ admits (ℤ/ℓ)² representatives QuaternionAlgebra.IsOrder.exists_zmod_prod_section_of_relIndex_eq_sq 3 below · cited by 2 · depth 27
• Inertia away from ℓ acts trivially on ℓ-power torsion QuaternionAlgebra.IsOrder.smul_eq_of_mem_inertiaSubgroupIn_of_mem_torsionBy_of_forall_isUnit_tensorProduct_padic 20 below · cited by 1 · depth 27
• Endomorphisms of ℂ² commuting with an order are homotheties QuaternionAlgebra.IsOrder.exists_eq_smul_of_forall_mulVec_comm 1 below · cited by 1 · depth 28
• Standard coordinates for two-dimensional complex Λ-modules QuaternionAlgebra.IsOrder.exists_linearEquiv_apply_eq_mulVec_map_of_finrank_eq_two 1 below · cited by 1 · depth 28
• Strong approximation for norm-one units, indefinite rational case QuaternionAlgebra.IsOrder.exists_nrd_eq_one_and_eq_finiteIdeleDiagonal_mul_mul_of_forall_nrd_eq_one_of_forall_isUnit 20 below · cited by 4 · depth 28
• Period lattice of an order is a full lattice in ℂ² QuaternionAlgebra.IsOrder.qmPeriodMap_injective_and_exists_basis_qmPeriodLattice_eq_span 2 below · cited by 8 · depth 28
• Globalising a level-N structure to an Eichler order QuaternionAlgebra.IsOrder.exists_isMaximalOrder_isEichlerOrder_forall_localBox_eq_of_forall_exists_isMaximalOrder_localBox_eq 31 below · cited by 1 · depth 29
• Strong approximation at a split place for indefinite quaternion orders QuaternionAlgebra.IsOrder.exists_ne_neg_one_forall_exists_nrd_eq_one_tmul_eq_add_smul_of_forall_isUnit 8 below · cited by 2 · depth 29
• Idelic factorisation of norm-one quaternion ideles from local density QuaternionAlgebra.IsOrder.exists_nrd_eq_one_and_eq_finiteIdeleDiagonal_mul_of_forall_exists_nrd_eq_one_tmul_eq_add_smul 10 below · cited by 1 · depth 29
• Index ℓ² of the left ideal Λ t when nrd(t)=ℓ QuaternionAlgebra.IsOrder.exists_submodule_forall_mem_iff_mul_eq_relIndex_eq_sq_of_nrd_eq 2 below · cited by 1 · depth 29
• Transport of a left Λ-line modulo ℓ along w QuaternionAlgebra.IsOrder.exists_submodule_forall_mem_iff_mul_mem_relIndex_eq_sq_of_mul_sub_one_eq_smul 0 below · cited by 1 · depth 29
• Finiteness of bounded elements of a quaternion order QuaternionAlgebra.IsOrder.finite_setOf_mem_forall_abs_apply_le 2 below · cited by 1 · depth 29
• One non-central approximable element suffices at a split place QuaternionAlgebra.IsOrder.forall_exists_nrd_eq_one_tmul_eq_add_smul_of_exists_ne_neg_one_of_ne_zero 8 below · cited by 2 · depth 29
• Right translation by a unit preserves the level identity QuaternionAlgebra.IsOrder.forall_exists_smul_add_mul_iff_mul_of_isUnitOf_right 0 below · cited by 1 · depth 29
• Orders in a rational quaternion algebra: conjugates, integral reduced trace and norm QuaternionAlgebra.IsOrder.star_mem_and_exists_int_trd_nrd 0 below · cited by 6 · depth 29
• Rigidity of unital multiplicative maps from an order to M₂(ℤ/N) QuaternionAlgebra.IsOrder.surjective_and_apply_eq_zero_iff_of_linearMap_matrix_zmod 0 below · cited by 1 · depth 29
• Reduced trace and χ+χ^q at a ramified prime QuaternionAlgebra.IsOrder.apply_add_pow_eq_intCast_of_add_star_eq_of_forall_isUnit 2 below · cited by 1 · depth 30
• Conjugating integral elements into d⁻¹O in a division quaternion algebra QuaternionAlgebra.IsOrder.exists_forall_exists_units_smul_conj_mem_of_int_trd_nrd_of_forall_isUnit 0 below · cited by 1 · depth 30
• Local Borel frame for an Eichler suborder at p ∥ N QuaternionAlgebra.IsOrder.exists_localBox_iff_and_localBox_iff_conj_diagonal_of_linearMap_matrix_zmod 4 below · cited by 1 · depth 30
• Casimir elements of a rational quaternion order multiply to integers QuaternionAlgebra.IsOrder.casimir_mul_mem_range_intCast_and_exists_casimir_mul_ne_zero 3 below · cited by 1 · depth 31
• Local box of a preimage order under an injective map QuaternionAlgebra.IsOrder.mem_localBox_iff_forall_rTensor_entryLinearMap_comp_mem_localBox 3 below · cited by 1 · depth 32
• Ohta's theorem for inertia over a discrete valuation ring QuaternionAlgebra.IsOrder.smul_eq_of_mem_inertiaSubgroupIn_of_mem_torsionBy_of_forall_isUnit_tensorProduct_padic_of_isDiscreteValuationRing 20 below · cited by 1 · depth 32
• Integral functionals on a quaternion order are reduced-trace forms QuaternionAlgebra.IsOrder.existsUnique_forall_intCast_eq_trd_mul_of_isIndefiniteRamifiedExactlyAt 5 below · cited by 1 · depth 38