Learning path

Each declaration appears after its prerequisites.

1. knownin1980s knownin1980s is a term which provides a proof of an arbitrary proposition
2. Mazur_statement Mazur's bound for the size of the torsion subgroup of an elliptic curve over the rationals
3. Odlyzko_statement An "Odlyzko bound" for the root discriminant of a totally complex number field of degree 18 and above
4. MaximalPQuotient The maximal p-quotient of a group
5. MaximalPQuotient.mk Quotient map into the maximal p-quotient of a group
6. Nat.exists_coprime_and_dvd_pow Also see IsPrincipalIdealRing.exists_isCoprime_and_dvd_pow
7. MaximalPQuotient.isPGroup_of_isMulTorsion The "maximal p-quotient" of (ℤ, +) is ℤ/⋂ₙ pⁿℤ = ℤ, not a p-group
8. Subgroup.quotientKerEquivMap First isomorphism theorem restricted to a subgroup
9. Subgroup.prodToSupOfRight If K is contained in the centralizer of H, then H ⊔ K is given by HK and the map H × K → HK is a group homomorphism
10. QuotientGroup.kerLift' The induced map from the quotient by the kernel to the codomain
11. MonoidHom.liftOfRightInverseAux' Auxiliary definition used to define liftOfRightInverse
12. TotallyDefiniteQuaternionAlgebra.Dfx Dfx is an abbreviation for $(D\otimes_F\mathbb{A}_F^\infty)^\times.$
13. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm This definition is made in mathlib-generality but is not the definition of a weight 2 automorphic form unless Dˣ is compact mod centre at infinity
14. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.zero The zero automorphic form for a totally definite quaterion algebra
15. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.neg Negation on the space of automorphic forms over a totally definite quaternion algebra
16. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.add Addition on the space of automorphic forms over a totally definite quaternion algebra
17. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.groupSMul The adelic group action on the space of automorphic forms over a totally definite quaternion algebra
18. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ringSMul The scalar action on the space of weight 2 automorphic forms on a totally definite quaternion algebra
19. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mapₗ Mapping an automorphic form along a linear map
20. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct The structure of an compact open U, and a continuous character on U that is trivial on 𝔸ᶠˣ
21. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA U 𝔸ᶠˣ of a LevelStruct
22. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.χA The character extended onto U 𝔸ᶠˣ
23. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Δ Δ_g := U 𝔸ˣ ∩ g⁻¹ Dˣ g
24. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.range_units_le_range Fˣ ≤ Δ_g
25. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isFiniteRelIndex_Δ [Δ_g : Fˣ] is finite
26. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex The index [U 𝔸ˣ ∩ g⁻¹ Dˣ g : Fˣ] as a function on Dˣ\GL₂(𝔸)/U
27. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form The subspace of modular forms of a given level
28. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formSubmodule Should not be used directly
29. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mkForm A constructor for forms in S(U, χ)
30. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.mkFormA A constructor for forms in S(U, χ) which instead asks for behaviour on U 𝔸ˣ
31. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map Mapping a LevelStruct along a ring hom
32. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsSufficientlySmall A level struct is sufficiently small if the associated character has finite order coprime to [Δ_g : Fˣ] for all g
33. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formEquivOfSection Given a section to the projection Dˣ＼GL₂(𝔸ᶠ[F])／U → GL₂(𝔸ᶠ[F]), S(U, χ) is isomorphic to the finite free module with basis Dˣ＼GL₂(𝔸ᶠ[F])／U
34. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formEquiv If U is sufficiently small, S(U, χ) is isomorphic to the finite free module with basis Dˣ＼GL₂(𝔸ᶠ[F])／U
35. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct._root_.TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.levelStruct A somewhat arbitrarily chosen level of an automorphic form
36. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.IsFinite Actually true for all totally definite quaternion algebra D but the instance is provided elsewhere
37. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMap Mapping automorphic forms of a fixed level along a linear map
38. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formCongr Mapping automorphic forms of a fixed level along a linear equiv
39. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMapₗ formMap as a linear map
40. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensor If U is sufficiently small, then M ⊗ S(U, N) = S(U, M ⊗ N)
41. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar If U is sufficiently small, then M ⊗ S(U, R) = S(U, M)
42. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.restrict Restriction of LevelStruct to an open subset
43. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Normal (U, χ) is normal in (U', χ') if U ≤ U' is normal and χ'|_U = χ
44. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct A way to construct LevelStruct via a family of local level structs on finitely many finite places
45. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct The LevelStruct constructed via a LocalLevelStruct
46. TotallyDefiniteQuaternionAlgebra.finite_doubleCoset For any open U ⊆ GL₂(𝔸_F), Dˣ\GL₂(𝔸_F)/U is finite
47. FixedPoints.submodule FixedPoints as a submodule
48. FixedPoints.module Probably this should be a submodule instance and then get module instance for free
49. AbstractHeckeOperator.eq_finsum_quotient_out_of_bijOn' If a is fixed by V then ∑ᶠ g ∈ s, g • a is independent of the choice s of coset representatives in G for a subset of G ⧸ V
50. AbstractHeckeOperator.heckeOperator.toFun The Hecke operator T_g = [UgV] : A^V → A^U associated to the double coset UgV
51. AbstractHeckeOperator.heckeOperator.addMonoidHom The Hecke operator T_g = [UgV] : A^V → A^U packaged as an additive monoid homomorphism
52. AbstractHeckeOperator.heckeOperator The Hecke operator T_g = [UgV] : A^V → A^U as an R-linear map, where R is any ring acting on A and commuting with the G-action
53. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.heckeOperatorL_tensor Hecke operators are preserved under the identification 𝒮²(U, χ; M ⊗ N) ≃ M ⊗ 𝒮²(U, χ; N)
54. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.heckeOperator_eq_lTensor Hecke operators are preserved under the identification 𝒮²(U, χ; M) ≃ M ⊗ 𝒮²(U, χ; R)
55. TotallyDefiniteQuaternionAlgebra.U₁Data The U₁ we will be considering needs the following input:
56. TotallyDefiniteQuaternionAlgebra.HeckeOperator.T The Hecke operator T_v as an R-linear map from M-valued quaternionic weight 2 automorphic forms of level U_1(S₀)
57. TotallyDefiniteQuaternionAlgebra.HeckeOperator.U The Hecke operator U_{v,α} associated to the matrix (α 0;0 1) at v, considered as an R-linear map from R-valued quaternionic weight 2 automorphic forms of level U_1(S)
58. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra Documented declaration: HeckeAlgebra
59. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T The Hecke operator Tᵥ as an element of the Hecke algebra
60. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.U The Hecke operator Uᵥ,ₐ as an element of the Hecke algebra
61. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.apply_eq_smul Note: This breaks the abstraction boundary that HeckeAlgebra is defined as a subtype under the hood
62. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.diag The matrix element diag[α, 1]
63. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotent_mem_localTameLevel Show that unipotent t is in U1 v for t ∈ O_v
64. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag The matrix element (unipotent t) * (diag α hα) = !![α, t; 0, 1]
65. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotentMulDiag_inv_mul_unipotentMulDiag !![α t₁; 0 1]⁻¹ * [α t₂; 0 1] = [1 (t₂ - t₁) / α; 0 1]
66. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.unipotentMulDiagU1 For each t ∈ O_v / αO_v, the left coset unipotentMulDiag U1 for a lift of t to O_v
67. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.unipotentMulDiagU1_injective Distinct t give distinct unipotent_mul_diagU1, i.e. we have a disjoint union
68. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.range_unipotentMulDiagU1 Each coset in U1diagU1 is of the form unipotent_mul_diagU1 for some t ∈ O_v
69. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.bijOn_unipotentMulDiagU1 The double coset space U1diagU1 is the disjoint union of unipotent_mul_diagU1 as t ranges over O_v / αO_v
70. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.innerSummand The summand appearing in the Petersson inner product
71. TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.haarQuot The haar measure on GL₂(𝔸ᶠ[F]) that gives Π GL₂(𝒪ᵥ) measure one
72. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform Type parametrising eigen spaces of the anemic hecke algebra on S(U, ℂ)
73. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenspace The eigenspace parametrised by an Eigenform
74. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenvalue The Tₚ-eigenvalue of an eigenform
75. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.integers The subring of ℂ generated by the eigenvalues of an eigenform
76. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.toIntegers The induced map of an Eigenform from an hecke algebra to its integers
77. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.prime The (minimal) prime corresponding to an eigenform
78. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.primeQuotient 𝕋/𝔭(f) = 𝒪(f)
79. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.toProdEigenform The embedding of the anemic Hecke algebra into a product of domains, indexed by eigenforms
80. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Pi.subalgebraEquiv There is a correspondence between K-subalgebras of Kⁿ and partitions of n, where for each set in the partition we take the diagonal subalgebra
81. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.tensorEquivPi The complex anemic Hecke algebra is isomorphic to a product of copies of ℂ's, one for each eigenform
82. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.equivAlgHom The eigenforms corresponds exactly to maps from 𝕋 to ℂ
83. TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.exists_le_of_isPrime linter complained that [P.IsPrime] wasn't needed, so this lemma is now poorly-named
84. Set.matrixEquiv Set.matrix is equivalent to matrices on the subtype
85. Subring.matrixEquiv Subring.matrix is equivalent to matrices on the subtype
86. Algebra.norm_one_tmul Finiteness not necessary?
87. ContinuousAddEquiv.smul smul as a ContinuousAddEquiv
88. MulOpposite.opMeasurableEquiv MulOpposite.op as a MeasurableEquiv
89. Units.opContinuousMulEquiv Units.opEquiv (taking x to x) as a ContinuousMulEquiv
90. MulDistribMulAction.toContinuousMulEquiv smul as a ContinuousMulEquiv
91. Nat.three_dvd_or_four_dvd_or_prime_dvd
92. FermatLastTheorem.of_p_ge_5 It suffices to prove FLT for primes at least 5 after Nat.three_dvd_or_four_dvd_or_prime_dvd
93. PNat.pow_add_pow_ne_pow_of_FermatLastTheorem Fermat's Last Theorem as stated in mathlib (a statement FermatLastTheorem about naturals) implies Fermat's Last Theorem stated in terms of positive integers
94. Hurwitz Hurwitz integers in the quaternions
95. Hurwitz.toQuaternion The embedding of the Hurwitz integers into the rational quaternions
96. Hurwitz.fromQuaternion Rounds a quaternion to a nearby Hurwitz integer; serves as a left inverse to toQuaternion
97. Hurwitz.zero The Hurwitz number 0
98. Hurwitz.one The Hurwitz number 1
99. Hurwitz.neg The negation -z of a Hurwitz number
100. Hurwitz.neg_re how neg interacts with re and im_*
101. Hurwitz.neg_im_o how neg interacts with re and im_*
102. Hurwitz.neg_im_i how neg interacts with re and im_*
103. Hurwitz.neg_im_oi how neg interacts with re and im_*
104. Hurwitz.add addition z+w of complex numbers
105. Hurwitz.add_re basic properties
106. Hurwitz.add_im_o basic properties
107. Hurwitz.add_im_i basic properties
108. Hurwitz.add_im_oi basic properties
109. Hurwitz.mul Multiplication z*w of two Hurwitz numbers
110. Hurwitz.mul_re how mul reacts with re and im
111. Hurwitz.starRing Conjugate; sends $a+bi+cj+dk$ to $a-bi-cj-dk$
112. Hurwitz.norm The norm of a Hurwitz integer: the integer z * star z, equivalently the squared absolute value of the corresponding quaternion
113. HurwitzHat The base change of the Hurwitz quaternions to ZHat
114. HurwitzRat The quaternion algebra ℚ + ℚi + ℚj + ℚk
115. HurwitzRatHat The "profinite Hurwitz quaternions" over the finite adeles of ℚ; a free rank 4 module generated by 1, i, j, and (1+i+j+k)/2
116. HurwitzRatHat.j₁ The inclusion from D=ℚ+ℚi+ℚj+ℚk to D ⊗ 𝔸, with 𝔸 the finite adeles of ℚ
117. HurwitzRatHat.j₂ The inclusion from the profinite Hurwitz quaternions to to 𝔸+𝔸i+𝔸j+𝔸k, with 𝔸 the finite adeles of ℚ
118. HurwitzRatHat.canonicalForm should I rearrange tensors?
119. ZHat We define the profinite completion of ℤ explicitly as compatible elements of ℤ/Nℤ for all positive integers N
120. ZHat.toZMod The canonical "reduce mod M" map from ZHat to ℤ/Mℤ
121. ZHat.e A nonarchimedean analogue `0!
122. ZHat.e_not_in_Int Nonarchimedean $e$ is not an integer
123. ZHat.torsionfree ZHat is torsion-free
124. ZHat.multiples LaTeX proof in the notes
125. ZHat.nat_dense ZHat has division by positive naturals, with remainder a smaller natural
126. QHat The "profinite completion" of ℚ is defined to be ℚ ⊗ ZHat, with ZHat the profinite completion of ℤ
127. QHat.IsCoprime An element z of ℤ̂ is coprime to N if its image in ℤ/Nℤ is a unit
128. QHat.i₂ The canonical inclusion ℤ̂ → ℚ̂ := ℚ ⊗_ℤ ℤ̂ sending z to 1 ⊗ z
129. QHat.i₁ The canonical inclusion ℚ → ℚ̂ = ℚ ⊗_ℤ ℤ̂ sending q to q ⊗ 1
130. QHat.ratsub The image of ℚ inside ℚ̂ as an additive subgroup
131. QHat.zHatsub The image of ℤ̂ inside ℚ̂ as an additive subgroup
132. QHat.zsub The image of ℤ inside ℚ̂ as an additive subgroup
133. QHat.unitsratsub The image of ℚˣ inside ℚ̂ˣ as a subgroup
134. QHat.unitszHatsub The image of ℤ̂ˣ inside ℚ̂ˣ as a subgroup
135. QHat.unitszsub The image of ℤˣ inside ℚ̂ˣ as a subgroup
136. QHat.unitsrat_join_unitszHat this needs that ℤ is a PID
137. IsDedekindDomain.HeightOneSpectrum.exists_adicValued_mul_sub_le Given a, b ∈ A and v b ≤ v a we can find y in A such that y is close to a / b by the valuation v
138. IsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_integers The closure of A in K_v is 𝒪_v
139. IsDedekindDomain.HeightOneSpectrum.denseRange_of_integerAlgebraMap A is dense in 𝒪_v
140. IsDedekindDomain.HeightOneSpectrum.exists_adicValued_sub_lt_of_adicCompletionInteger An element of 𝒪_v can be approximated by an element of A
141. IsDedekindDomain.HeightOneSpectrum.completionIdeal The maximal ideal of the integers of the completion of v
142. IsDedekindDomain.HeightOneSpectrum.ResidueFieldToCompletionResidueField The canonical ring homomorphism from A / v to 𝓞ᵥ / v, where 𝓞ᵥ is the integers of the completion Kᵥ of the field of fractions of A
143. IsDedekindDomain.HeightOneSpectrum.ResidueFieldEquivCompletionResidueField The canonical isomorphism from A / v to 𝓞ᵥ / v, where 𝓞ᵥ is the integers of the completion Kᵥ of the field of fractions K of A
144. IsDedekindDomain.HeightOneSpectrum.exists_forall_adicValued_sub_lt An element of ∏_{v ∈ s} 𝒪_v, with s finite, can be approximated by an element of A
145. IsDedekindDomain.HeightOneSpectrum.closureAlgebraMapIntegers_eq_prodIntegers The closure of A in ∏_{v ∈ s} K_v is ∏_{v ∈ s} 𝒪_v
146. IsDedekindDomain.HeightOneSpectrum.denseRange_of_prodAlgebraMap If s is finite then K in dense in ∏_{v ∈ s} K_v
147. IsDedekindDomain.HeightOneSpectrum.Extension._root_.WithVal.semialgebraMap The map (R,v) → (S,w) as a semialgebra map over R → S (which is the same map!)
148. IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom If w of L divides v of K, underSemialgHom v w pf is the canonical map Kᵥ → L_w lying above K → L
149. IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_coe The square with sides K → K_v → L_w and K → L → L_w commutes
150. IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_continuous The map K_v → L_w is continuous
151. IsDedekindDomain.HeightOneSpectrum.Extension.valued_adicCompletionSemialgHom The local ramification index for the extension L_w/K_v is equal to the global ramification index for the extension w/v
152. IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionSemialgHom_image_adicCompletionIntegers The canonical map K_v → L_w sends 𝓞_v to 𝓞_w
153. IsDedekindDomain.HeightOneSpectrum.adicCompletion.semialgHomPi The canonical map K_v → ∏_{w|v} L_w extending K → L
154. IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange The canonical ring homomorphism L ⊗_K K_v → ∏_{w|v} L_w as an L-algebra map
155. IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight The canonical ring homomorphism L ⊗_K K_v → ∏_{w|v} L_w as an K_v-linear map
156. IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight_surjective The canonical map L ⊗[K] K_v → ∏_{w|v} L_w is surjective
157. IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopology L_w has the K_v-module topology
158. IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsModuleTopologyPi ∏_{w|v} L_w has the K_v-module topology
159. IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeRight_isOpenQuotientMap tensorAdicCompletionComapLinearMap is continuous, open and surjective
160. IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo The canonical B-algebra map B ⊗[A] 𝓞_v → L ⊗[K] K_v
161. IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_range_subset_closure The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is contained in the closure of the image of B
162. IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersTo_isClopen_range The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is clopen
163. IsDedekindDomain.HeightOneSpectrum.range_tensorAdicCompletionIntegersTo_eq_closure_range_algebraMap The image of B ⊗[A] 𝓞_v in L ⊗[K] K_v is the closure of the image of B
164. IsDedekindDomain.HeightOneSpectrum.pi_adicCompletionIntegers_eq_closure_range_algebraMap The B-subalgebra ∏_{w|v} 𝓞_w of ∏_{w|v} L_w is the closure of the image of B
165. IsDedekindDomain.HeightOneSpectrum.isClosed_baseChange_image_closure_range_algebraMap The image of B ⊗[A] 𝓞_v (the closure of B) in ∏_w L_w is closed
166. IsDedekindDomain.HeightOneSpectrum.range_baseChange_comp_tensorAdicCompletionTo_eq_pi The image of B ⊗[A] 𝓞_v in ∏_w L_w is ∏_w 𝓞_w
167. IsDedekindDomain.HeightOneSpectrum.Extension.adicCompletionIntegersRingHom The restriction of adicCompletionSemialgHom to a map 𝓞_v → 𝓞_w
168. IsDedekindDomain.HeightOneSpectrum.tensorAdicCompletionIntegersToPiRight The O_v-linear map from B ⊗[A] 𝓞ᵥ to Π v ∣ w, L_w
169. IsDedekindDomain.HeightOneSpectrum.Extension.tensorAdicCompletionIntegersToAdicCompletion The map B ⊗ 𝓞_v → L_w for w an extension of v given by the algebra maps
170. IsDedekindDomain.HeightOneSpectrum.Extension.tensorAdicCompletionIntegersToAdicCompletion_range_eq_integers The range of adicCompletionIntegers.tensorToAdicCompletion is 𝓞_w
171. IsDedekindDomain.HeightOneSpectrum.adicCompletion.liesOver_completionIdeal The maximal ideal of 𝒪_w lies over the maximal ideal of 𝒪_v
172. IsDedekindDomain.HeightOneSpectrum.adicCompletion.ramificationIdx_eq_ramificationIdx The local ramification index of L_w/K_v equals the global ramification index of w/v
173. IsDedekindDomain.HeightOneSpectrum.adicCompletion.inertiaDeg_eq_inertiaDeg The local inertia degree of L_w/K_v equals the global inertia degree of w/v
174. IsDedekindDomain.HeightOneSpectrum.adicCompletion.ramificationIdx_mul_inertiaDeg_eq_finrank Documented declaration: ramificationIdx_mul_inertiaDeg_eq_finrank
175. IsDedekindDomain.HeightOneSpectrum.adicCompletion.finrank_tensorProduct_adicCompletion_eq_finrank_pi_adicCompletion L ⊗[K] K_v and ∏_{w|v} L_w have equal dimensions
176. IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChange_bijective The canonical map L ⊗[K] K_v → ∏_{w|v} L_w is bijective
177. IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeAlgEquiv The L-algebra isomorphism L ⊗[K] K_v ≅ ∏_{w|v} L_w
178. IsDedekindDomain.HeightOneSpectrum.adicCompletion.baseChangeContinuousAlgEquiv The continuous L-algebra isomorphism L ⊗[K] K_v ≅ ∏_{w|v} L_w
179. IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerBaseChangeLinearEquiv The B-module isomorphism B ⊗[A] K_v ≅ ∏_{w|v} L_w
180. IsDedekindDomain.HeightOneSpectrum.adicCompletion.integerSubmodule 𝓞_v as an A-submodule of K_v
181. IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.tensorCoe The canonical B-linear map B ⊗[A] 𝓞_v → B ⊗[A] K_v
182. IsDedekindDomain.FiniteAdeleRing.mapRingHom The ring homomorphism 𝔸_K^∞ → 𝔸_L^∞ for L/K an extension of number fields
183. IsDedekindDomain.FiniteAdeleRing.mapSemialgHom The ring homomorphism 𝔸_K^∞ → 𝔸_L^∞ for L/K an extension of number fields, as a morphism lying over the canonical map K → L
184. IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul Utility class which specialises RestrictedProduct.FiberwiseSMul to the case of finite adele rings
185. IsDedekindDomain.FiniteAdeleRing.tensorEquivTensor The canonical linear isomorphism L ⊗[K] 𝔸_K^∞ ≅ B ⊗[A] 𝔸_K^∞
186. IsDedekindDomain.FiniteAdeleRing.tensorEquivRestrictedProduct The B-linear isomorphism φ : B ⊗[K] 𝔸_K^∞ ≅ ∏'_v [B ⊗[A] K_v, B ⊗[A] 𝓞_v] given by φ (b ⊗ x) v = b ⊗ (x v)
187. IsDedekindDomain.FiniteAdeleRing.restrictedProductTensorProductEquivRestrictedProductProd The B-linear isomorphism ∏'_v [B ⊗[A] K_v, B ⊗[A] 𝓞_v] ≅ ∏'_v [∏_{w|v} L_w, ∏_{w|v} 𝓞_w] given by adicCompletionComapIntegerLinearEquiv
188. IsDedekindDomain.FiniteAdeleRing.restrictedProductProdEquiv The B-linear isomorphism ∏'_v [∏_{w|v} L_w, ∏_{w|v} 𝓞_w] → 𝔸_L^∞ given by RestrictedProduct.flattenEquiv'
189. IsDedekindDomain.FiniteAdeleRing.baseChangeLinearEquiv The L-linear isomorphism L ⊗ A_K^∞ ≅ A_L^∞ given by composing the previous four maps
190. IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv The L-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞
191. IsDedekindDomain.FiniteAdeleRing.baseChangeAdeleAlgEquiv The 𝔸_K^∞-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞
192. IsDedekindDomain.FiniteAdeleRing.piAdicIntegerSubmodule ∏_{w∣v} 𝓞_w as an 𝓞_v-submodule of ∏_{w∣v} L_w
193. IsDedekindDomain.FiniteAdeleRing.restrictedProductPiEquiv The continuous 𝔸 K-Linear equivalence between ∏'_v ∏_{w∣v} L_w and 𝔸 L given by reaindexing the elements
194. IsDedekindDomain.FiniteAdeleRing.baseChangeAdeleContinuousAlgEquiv The continuous 𝔸_K^∞-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞
195. IsDedekindDomain.FiniteAdeleRing.baseChangeContinuousAlgEquiv The continuous L-algebra isomorphism L ⊗_K 𝔸_K^∞ ≅ 𝔸_L^∞
196. IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer A uniformiser associated to v in the completion Kᵥ
197. IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersUniformizer A uniformiser associated to v in the integers of the completion Kᵥ
198. IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizerUnit A uniformiser associated to v in the units of the completion Kᵥ
199. IsDedekindDomain.FiniteAdeleRing.localUniformiser localUniformiser v is an adele which is 1 at all finite places except v, where it is a uniformiser
200. IsDedekindDomain.FiniteAdeleRing.localUniformiserUnit localUniformiser v is an idele which is 1 at all finite places except v, where it is a uniformiser
201. IsDedekindDomain.FiniteAdeleRing.localUnit localUnit K α for α : (v.adicCompletion K)ˣ, is the finite idele which is α at v and 1 elsewhere
202. directSumPiEquivPiSum ⨁ⱼ(∏ᵢ Nᵢⱼ) ≅ ∏ᵢ(⨁ⱼNᵢⱼ) if j ranges over a finite index set and i over an arbitrary index set
203. freeModuleTensorPiEquiv The isomorphism M ⊗ ∏ᵢ Nᵢ ≅ (B →₀ R) ⊗ ∏ᵢ Nᵢ, where M is assumed free and B is the basis of M given by Lean's global axiom-of-choice operator
204. finsuppLeftTensorPiEquivPiTensor If B is finite then tensoring by the free module with basis B commutes with arbitrary products
205. tensorPiEquivFinitefreeModule The isomorphism Πᵢ ((B →₀ R) ⊗ Nᵢ) ≅ Πᵢ (M ⊗ Nᵢ) where M is assumed free and B is the basis of M given by Lean's global axiom-of-choice operator
206. tensorPiEquivPiTensor Tensoring with a finite free module commutes with arbitrary products
207. tensorPiEquivPiTensor' Tensoring with a finitely-presented module commutes with arbitrary products
208. IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent Documented declaration: localcomponent
209. IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply Documented declaration: localcomponent_apply
210. IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv Documented declaration: localcomponentEquiv
211. RestrictedProduct.rangeLTensor M ⊗_R (L i) as an R-submodule of M ⊗_R (N i)
212. RestrictedProduct.rangeLTensorLeft M ⊗_R (L i) as an M-submodule of M ⊗_R (N i)
213. RestrictedProduct.lTensor The R-linear map φ : M ⊗_R ∏'_i [N i, L i]_[𝓕] → ∏'_i [M ⊗_R (N i), M ⊗_R (L i)]_[𝓕] given by φ (m ⊗ n) i = m ⊗ (n i)
214. RestrictedProduct.lTensorLeft The M-linear map φ : M ⊗_R ∏'_i [N i, L i]_[𝓕] → ∏'_i [M ⊗_R (N i), M ⊗_R (L i)]_[𝓕] given by φ (m ⊗ n) i = m ⊗ (n i)
215. RestrictedProduct.tmulEquivRangeLTensor R-Linear isomorphism between M ⊗_R (L i) and rangeLTensor R M N L i
216. RestrictedProduct.lTensorPrincipalEquiv R-Linear isomorphism that's propositionally equal to lTensor
217. RestrictedProduct.lTensorEquiv The R-linear isomorphism given by lTensor when M is a finite flat R-module
218. RestrictedProduct.lTensorEquivLeft The M-linear isomorphism given by lTensor when M is a finite flat R-module
219. IsDedekindDomain.HeightOneSpectrum.Extension Documented declaration: Extension
220. IsDedekindDomain.HeightOneSpectrum.intValuation_comap If w | v then for a ∈ A we have w(a)=v(a)^e where e is the ramification index
221. IsDedekindDomain.HeightOneSpectrum.valuation_comap If w | v then for x ∈ K we have w(x)=v(x)^e where e is the ramification index
222. IsDedekindDomain.HeightOneSpectrum.Extension.finite There are only finitely many nonzero primes of B above a nonzero prime of A
223. IsDedekindDomain.HeightOneSpectrum.Extension.fintype There are only finitely many nonzero primes of B above a nonzero prime of A
224. IsDedekindDomain.HeightOneSpectrum.preimageComapFinset Given an inclusion of Dedekind domains A → B, making B finite over A, this is the preimage of a Finset of finite places of A, as a Finset of finite places of B
225. IsDedekindDomain.HeightOneSpectrum.Extension.equivPrimesOver The primes of B extending v are precisely the primes of B lying over v.asIdeal
226. IsDedekindDomain.HeightOneSpectrum._root_.Ideal.sum_ramification_inertia_extensions Ideal.sum_ramification_inertia_eq_finrank, rewritten as a sum over extensions
227. IsDedekindDomain.LinearEquivTensorProduct The canonical K-linear isomorphism L ≅ K ⊗ B
228. IsDedekindDomain.linearEquivTensorProductModule The canonical A-linear isomorphism L ⊗ M ≅ B ⊗ M for any K-module M
229. IsDedekindDomain.linearEquivTensorProductModuleLeft The canonical B-linear isomorphism L ⊗ M ≅ B ⊗ M for any K-module M
230. InverseLimit InverseLimit G f is the Inverse Limit of the objects G i glued by functions f
231. InverseLimit.toComponent toComponent G f i is the canonical function from the inverse limit of the G_j to G_i
232. InverseLimit.toComponentMonoidHom MonoidHom version of toComponent G f i
233. InverseLimit.toComponentRingHom RingHom version of toComponent G f i
234. InverseLimit.toComponentLinearMap LinearMap version of toComponent G f i
235. InverseLimit.InverseSystemHom InverseSystemHom G f maps states that a indexed family of maps : W →G i have image in the InverseLimit G f subset of the product
236. InverseLimit.lift lift G f maps inverseSystemHom is the canonical function from W to the inverse limit of the G_j built by x ↦ Π maps_j x
237. InverseLimit.liftMonoidHom MonoidHom version of lift G f maps inverseSystemHom
238. InverseLimit.liftRingHom RingHom version of lift G f maps inverseSystemHom
239. InverseLimit.liftLinearMap LinearMap version of lift G f maps inverseSystemHom
240. Deformation.IsLocalProartinianAlgebra A local proartinian algebra is a topological ring that is local and proartinian, and that the induced map on the residue fields is bijective
241. Deformation.ProartinianCat The category of local proartinian algebras over 𝓞 with fixed residue field 𝕜
242. Deformation.ProartinianCat.of Make a ProartinianCat from an unbundled algebra
243. Deformation.ProartinianCat.Hom The type of morphisms in ProartinianCat 𝓞
244. Deformation.ProartinianCat.ofHom Typecheck an ContinuousAlgHom as a morphism in ProartinianCat
245. Deformation.ProartinianCat.ofEquiv Build an isomorphism in the category ProartinianCat R from a ContinuousAlgEquiv between Algebras
246. Deformation.ProartinianCat._root_.CategoryTheory.Iso.toContinuousAlgEquiv Build a ContinuousAlgEquiv from an isomorphism in the category ProartinianCat R
247. Deformation.ProartinianCat.self 𝓞 as a proartinian local algebra
248. Deformation.ProartinianCat.fromSelf The structure map of a proartinian local algebra as a morphism in the category
249. Deformation.ProartinianCat.isInitialSelf 𝓞 is initial in ProartinianCat
250. Deformation.ProartinianCat.residueField The residue field 𝕜 as a proartinian local algebra
251. IsTopologicalModule IsTopologicalModule R M states that the topology in M makes scalar multiplication and addition into continuous maps
252. IsProartinian A topological ring is proartinian if it is linearly topologized, complete hausdorff, and all its discrete quotients are artinian
253. IsResidueAlgebra IsResidueAlgebra 𝓞 indicates that A [Algebra 𝓞 A] has the same residue field as 𝓞
254. IsResidueAlgebra.algEquiv The isomorphism of residue fields for a residue algebra
255. Units.mapₜ The continuous group homomorphism on units induced by a ContinuousMonoidHom
256. ContinuousAlgHom.mapMatrix The ContinuousAlgHom between spaces of square matrices induced by an ContinuousAlgHom between their coefficients
257. ContinuousAlgHom.toContinuousMonoidHom Coerce a ContinuousAlgHom to ContinuousMonoidHom
258. Module.endSelf End_A(A) ≃ A
259. ContinuousMonoidHom.toHomUnits Given a ContinuousMonoidHom from a group to a monoid, we may lift it to map into the group of units of the monoid
260. Units.coeHomₜ Units.val as a ContinuousMonoidHom
261. ContinuousAlgEquiv.ofIsModuleTopology We can upgrade an AlgEquiv between algebras with the module topology into a ContinuousAlgEquiv
262. Deformation.repnFunctor repnFunctor n G 𝓞 is the functor taking R to continuous reps G → GLₙ(R)
263. Deformation.toRepresentation Turn an element in repnFunctor into an actual Representation
264. Deformation.flatFunctor The subfunctor of flat lifts
265. Deformation.unramifiedFunctor The subfunctor of unramified (at v) representations
266. Deformation.traceConditionFunctor The subfunctor of representations whose trace is 2 on ker(Iᵥ → k(v)ˣ)
267. Deformation.narrowTraceConditionFunctor The subfunctor of representations whose trace is 2 on Iᵥ
268. Deformation.detConditionFunctor The subfunctor of representations with det = εₗ
269. Deformation.SLiftFunctor The functor of S-lifts of ρ, consisting of representations of GL₂ satisfying: 1
270. Deformation.narrowSLiftFunctor The functor of narrow S-lifts of ρ, consisting of representations of GL₂ satisfying: 1
271. Deformation.narrowSLiftUniversalRing The universal lifting ring Rᵘⁿⁱᵛ representing the functor of narrow S-lifts
272. Deformation.narrowSLiftUniversalRingCorepresentableBy The universal lifting ring Rᵘⁿⁱᵛ represents the functor of narrow S-lifts
273. IsArithFrobAt.exists_of_isInvariant_of_profinite Let G be a finite group acting on S, and R be the fixed subring
274. GaloisRep GaloisRep K A M are the A-linear galois reps of a field K on the A-module M
275. FramedGaloisRep A framed galois rep is a galois rep with a distinguished basis
276. FramedGaloisRep.equivChar 1-dimensional framed galois reps are equivalent to (continuous) characters
277. GaloisRep.IsUnramifiedAt The class of galois reps unramified at v
278. GaloisRep.Space The underlying space of a galois rep
279. GaloisRep.HasFlatProlongationAt Documented declaration: HasFlatProlongationAt
280. GaloisRep.IsFlatAt A galois rep ρ : Γ K → Aut_A(M) is flat at v if A/I ⊗ M has a flat prolongation at v for all open ideals I
281. GaloisRep.toRepresentation A Galois representation is a representation (note that we are forgetting topological information here)
282. GaloisRep.IsIrreducible Irreducibility of a Galois representation over a field
283. GaloisRepFamily Documented declaration: GaloisRepFamily
284. GaloisRepFamily.isCompatible Documented declaration: isCompatible
285. IntegralClosure IntegralClosure R A is the integral closure of R in A as a type
286. Representation.IsAbsolutelyIrreducible IsAbsolutelyIrreducible ρ states that a given Representation ρ over a field k is absolutely irreducible, meaning that all the possible base change extensions are irreducible
287. CategoryTheory.Subfunctor.ofIsTerminal The subfunctor defined by pulling back a subset of the terminal component
288. NumberField.AdeleRing.DivisionAlgebra.Aux.Df Df is notation for D ⊗ 𝔸_K^∞
289. NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx Dfx is notation for (D ⊗ 𝔸_K^∞)ˣ
290. NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf Dinf is notation for D ⊗ 𝔸_K^∞
291. NumberField.AdeleRing.DivisionAlgebra.Aux.Dinfx Dinfx is notation for (D ⊗ 𝔸_K^∞)ˣ
292. NumberField.AdeleRing.DivisionAlgebra.Aux.incl The inclusion Dˣ → D_𝔸ˣ as a group homomorphism
293. NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁ The inclusion Dˣ → (D ⊗ 𝔸_K^∞)ˣ as a group homomorphism
294. NumberField.AdeleRing.DivisionAlgebra.Aux.inclKn𝔸Kn The inclusion of K^n into 𝔸^n
295. NumberField.AdeleRing.DivisionAlgebra.Aux.DIso The K-algebra equivalence of D and K^n
296. NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸Iso The 𝔸_K-algebra equivalence of D_𝔸 and 𝔸_K^d
297. NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸IsoTop The topological 𝔸_K-linear equivalence D_𝔸 ≃ 𝔸_K^d
298. NumberField.AdeleRing.DivisionAlgebra.Aux.includeLeftSubgroup The additive subgroup D of D_𝔸
299. NumberField.AdeleRing.DivisionAlgebra.Aux.compact_includeLeft_subgroup we seem to have this twice?
300. NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight The K-algebra isomorphism D_𝔸 ≃ D_∞ × D_f -- adelic D is infinite adele D times finite adele D
301. NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight' The 𝔸_K linear map D_𝔸 ≃ D_∞ × D_f
302. NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight'' The continuous additive isomorphism D_𝔸 ≃ D_∞ × D_f
303. NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRightUnits The equivalence of the units of D_𝔸 and the product of the units of (D ⊗ 𝔸_K^f) and (D ⊗ 𝔸_K^∞)
304. NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjective For any positive real r, there's some ρ ∈ ℝˣ such that the haar character of (ρ, 1) ∈ D_f × D_∞ is r
305. NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_aux Left and right Haar characters agree for u : (Π vi : InfinitePlace K, (D ⊗[K] vi.Completion))ˣ
306. NumberField.InfiniteAdeleRing.realToCompletion The canonical ℝ-algebra structure on InfinitePlace.Completion
307. NumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensorAux tensorPiEquivPiTensor applied to Dinf, as a ℝ-linear equiv
308. NumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensor tensorPiEquivPiTensor applied to Dinf, as a continuous ℝ-linear equiv
309. NumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensorMulEquiv tensorPiEquivPiTensor applied to Dinf, as a mul equiv
310. NumberField.AdeleRing.DivisionAlgebra.Aux.Uf An auxiliary compact subset of D_𝔸^f with nonempty interior
311. NumberField.AdeleRing.DivisionAlgebra.Aux.Ui An auxiliary compact subset of D_∞ with nonempty interior
312. NumberField.AdeleRing.DivisionAlgebra.Aux.Efamily Documented declaration: Efamily
313. NumberField.AdeleRing.DivisionAlgebra.Aux.E An auxiliary set E used in the proof of Fujisaki's lemma
314. NumberField.AdeleRing.DivisionAlgebra.Aux.X An auxiliary set X used in the proof of Fukisaki's lemma
315. NumberField.AdeleRing.DivisionAlgebra.Aux.Y An auxiliary set Y used in the proof of Fukisaki's lemma
316. NumberField.AdeleRing.DivisionAlgebra.Aux.T An auxiliary set T used in the proof of Fukisaki's lemma
317. NumberField.AdeleRing.DivisionAlgebra.Aux.C An auxiliary set C used in the proof of Fukisaki's lemma
318. NumberField.AdeleRing.DivisionAlgebra.Aux.incl₂ The inclusion of ringHaarCharKer D_𝔸 into the product space D_𝔸 × D_𝔸ᵐᵒᵖ
319. NumberField.AdeleRing.DivisionAlgebra.Aux.M An auxiliary set used in the proof of compact_quotient'
320. NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot The map from ringHaarCharKer D_𝔸 to the quotient Dˣ \ ringHaarCharKer D_𝔸
321. NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁ The restriction of ringHaarCharKer D_𝔸 to (D ⊗ 𝔸_K^∞)ˣ via D𝔸_iso_prod_units
322. NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_equivariant the goal that comes up when you define the map Dˣ \ D_𝔸^(1) to Dˣ \ (Dfx K D) below using Quot.lift
323. NumberField.AdeleRing.DivisionAlgebra.Aux.inclD𝔸quot The obvious map Dˣ \ D_𝔸^(1) to Dˣ \ (Dfx K D)
324. NumberField.AdeleRing.DivisionAlgebra.compact_quotient Dˣ \ D_𝔸^{(1)} is compact
325. NumberField.AdeleRing.DivisionAlgebra._root_.NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact Dˣ \ D_𝔸^fˣ is compact
326. WeierstrassCurve.nTorsion The n-torsion subgroup of an elliptic curve E over k: the kernel of multiplication by n on the group of k-points of E
327. WeierstrassCurve.n_torsion_finite This theorem needs e.g. a theory of division polynomials
328. WeierstrassCurve.n_torsion_card This theorem needs e.g. a theory of division polynomials
329. group_theory_lemma This theorem was well-known in the early part of the 20th century
330. WeierstrassCurve.n_torsion_dimension I only need this if n is prime but there's no harm thinking about it in general I guess
331. WeierstrassCurve.Points.map The map on points for an elliptic curve over k induced by a morphism of k-algebras is a group homomorphism
332. WeierstrassCurve.galoisRepresentationSmul The Galois action on the points of an elliptic curve
333. WeierstrassCurve.galoisRepresentation The Galois action on the points of an elliptic curve
334. WeierstrassCurve.galoisRep The continuous Galois representation associated to an elliptic curve over a field
335. FreyPackage.freyCurveInt The Weierstrass curve over ℤ associated to a Frey package
336. FreyPackage.freyCurve The elliptic curve over ℚ associated to a Frey package
337. FreyCurve.j_valuation_of_bad_prime The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is a prime of bad reduction
338. FreyPackage Frey package
339. FreyPackage.of_not_FermatLastTheoremFor_p_ge_5 Given a counterexample a^p+b^p=c^p to Fermat's Last Theorem with p>=5 and prime, there exists a Frey package
340. FreyPackage.fermatLastTheoremFor_p_ge_5 Empty type of Frey packages gives FLT for p at least 5 after FreyPackage, FreyPackage.of_not_FermatLastTheoremFor_p_ge_5
341. FreyPackage.mazur Mazur step: the p-torsion of the Frey curve is irreducible (assumed) after FreyPackage, FreyPackage.freyCurve
342. GaloisRep.IsAutomorphicOfLevel Documented declaration: IsAutomorphicOfLevel
343. cyclic_base_change Cyclic base change
344. CyclotomicCharacterAux The cyclotomic character
345. CyclotomicCharacterZHat The Zhat-adic cyclotomic character
346. GaloisRepresentation.Z2bar Z2bar is the ring of integers of ℚ_[2]ᵃˡᵍ
347. GaloisRepresentation.IsHardlyRamified Documented declaration: IsHardlyRamified
348. GaloisRepresentation.IsHardlyRamified.lifts An irreducible mod p hardly ramified representation lifts to a p-adic one
349. GaloisRepresentation.IsHardlyRamified.mod_three A mod 3 hardly ramified representation is an extension of trivial by cyclo
350. GaloisRepresentation.IsHardlyRamified.three_adic A 3-adic hardly ramified representation has trace(Frob_p) = 1 + p for all p ≠ 2,3
351. IsDedekindDomain.bracketBilin The action of a Lie R-algebra on a Lie R-module, as an R-bilinear map
352. AutomorphicForm.GLn.action The action of the Lie algebra of left-invariant derivations on a Lie group G on smooth real-valued functions on G, viewed as a Lie algebra homomorphism
353. AutomorphicForm.GLn.LieModuleHom.baseChange Base change of a Lie module homomorphism f : M →ₗ⁅R,L⁆ N along a commutative algebra A over R
354. AutomorphicForm.GLn.LieHom.baseChange Base change of a Lie algebra homomorphism f : L →ₗ⁅R⁆ L' along a commutative algebra A over R
355. AutomorphicForm.GLn.actionTensorC Complexification of AutomorphicForm.GLn.action: the Lie action of the complexified Lie algebra on the complexification of smooth real functions on G
356. AutomorphicForm.GLn.actionTensorCAlg Extension of AutomorphicForm.GLn.actionTensorC to the universal enveloping algebra of the complexified Lie algebra
357. AutomorphicForm.GLn.actionTensorCAlg' Variant of actionTensorCAlg whose codomain is the ℂ-linear endomorphisms of the complexified function space
358. AutomorphicForm.GLn.actionTensorCAlg'2 Restriction of actionTensorCAlg' to the centre of the universal enveloping algebra
359. AutomorphicForm.GLn.Alg The universal enveloping algebra over ℂ of the complexified Lie algebra of G
360. AutomorphicForm.GLn.Z The centre of the universal enveloping algebra Alg G E
361. AutomorphicForm.GLn.actionTensorCAlg'3 The ℂ-algebra map from the centre of the universal enveloping algebra to the endomorphism algebra of complex-valued smooth functions on G
362. AutomorphicForm.GLn.IsSmooth A function on GL_n(𝔸_f) × GL_n(ℝ) is smooth if it is continuous, locally constant in the finite-adelic variable, and C^∞ in the archimedean variable
363. AutomorphicForm.GLn.s An auxiliary "size" function on invertible real matrices used in the slowly increasing condition; namely tr(MMᵀ) + tr(M⁻¹(M⁻¹)ᵀ)
364. AutomorphicForm.GLn.IsSlowlyIncreasing A function f : GL_n(ℝ) → ℂ is slowly increasing if there exist C, N such that ‖f M‖ ≤ C · s(M)^N for all M, where s is an auxiliary "size" function
365. AutomorphicForm.GLn.preweight A preweight for GLₙ is a continuous representation of the real orthogonal group O(n) on a finite-dimensional complex vector space
366. AutomorphicForm.GLn.preweight.fdRep The finite-dimensional ℂ-representation of O(n) associated to a preweight w
367. AutomorphicForm.GLn.Weight A weight for GLₙ: a preweight whose associated O(n)-representation is simple
368. AutomorphicForm.GLn._root_.RingHom.GL Functoriality of GLₘ: a ring homomorphism A →+* B induces a group homomorphism GLₘ(A) →* GLₘ(B) by applying it entrywise
369. AutomorphicForm.GLn.IsConstantOn The function f : GL_n(𝔸_f) × GL_n(ℝ) → ℂ is right-U-invariant in the finite-adelic variable, where U is an open compact subgroup
370. AutomorphicForm.GLn.annihilator The annihilator of an element a : M in the module of R-linear maps M →ₗ[R] N: those f with f a = 0
371. AutomorphicForm.GLn.AutomorphicFormForGLnOverQ Automorphic forms for GL_n/Q with weight ρ
372. AutomorphicForm.GLn.Weight.IsTrivial A GLₙ-weight ρ is trivial if it is the one-dimensional trivial representation
373. AutomorphicForm.GL0.ofComplex Make an automorphic form for GL₀/ℚ from a complex number
374. AutomorphicForm.GL0.classification The classification of automorphic forms for GL₀/ℚ: they are in bijection with ℂ
375. AutomorphicForm.GLn.ofComplex Make an automorphic form for GLₙ/ℚ of trivial weight ρ from a complex number z, returning the constant function with value z
376. AutomorphicForm.GLn.classification The classification of automorphic forms for GL₀/ℚ of weight ρ: they are in bijection with ℂ
377. MeasureTheory.mulEquivHaarChar_map_open Version of mulEquivHaarChar_smul_map without the regularity assumption In this case, the measures need only be equal on open sets
378. MeasureTheory._root_.WeaklyLocallyCompactSpace.of_isTopologicalGroup_of_isOpen_compactSpace_subgroup TODO this should be elsewhere note: it can't be an instance because typeclass inference can't find C
379. TensorProduct.RightActions.ContinuousLinearEquiv.baseChange The continuous A-linear map (A a topological ring, tensor products have the module topology) A ⊗[R] M ≃ A ⊗[R] N associated to an abstract R-linear isomorphism M ≃ N
380. LinearMap.toMatrix_basis mathlib?
381. NumberField.AdeleRing.units_mem_ringHaarCharacter_ker Left multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure
382. NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one Right multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure
383. FiniteAdeleRing.Aux.f Documented declaration: f
384. FiniteAdeleRing.Aux.g If ψ : (𝔸_K^f)^n ≃ (𝔸_K^f)^n is continuous and 𝔸_K^f-linear then g φ is the associated continuous additive isomorphism Πʳ[Kᵥ^n, 𝓞ᵥ^n] → Πʳ[Kᵥ^n,𝓞ᵥ^n]
385. FiniteAdeleRing.Aux.e If φ : Kᵥ ⊗[K] B ≃ Kᵥ ⊗[K] B is continuous and additive then f φ is the associated continuous additive isomorphism Kᵥ^n ≃ Kᵥ^n coming from the "canonical" K-basis of B
386. bLocal bLocal is v.adicCompletion K-basis for v.adicCompletion K ⊗[K] B
387. bGlobal bGlobal is FiniteAdeleRing (𝓞 K) K-basis for FiniteAdeleRing (𝓞 K) K ⊗[K] B
388. φLocalKvLinear TensorProduct.localcomponent φ as v.adicCompletion K-linear map
389. toMatrix_f The matrix reps of φ and f φ agree
390. FiniteAdeleRing.Aux.almost_always_mapsTo A (continuous) 𝔸_K^f-linear automorphism of 𝔸_K^f ⊗ B is "integral" at all but finitely many places
391. FiniteAdeleRing.Aux.almost_always_bijOn A (continuous) 𝔸_K^f-linear automorphism of 𝔸_K^f ⊗ B is "integral" at all but finitely many places
392. FiniteAdeleRing.Aux.f_g_local_global A diagram which obviously commutes, commutes
393. NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul left multiplication and right multiplication by a unit have the same Haar character on 𝔸_K^f ⊗ B
394. FiniteAdeleRing.TensorProduct.commLinearMap B ⊗ 𝔸_K^f ≃ 𝔸_K^f ⊗ B as 𝔸_K^f-modules
395. FiniteAdeleRing.TensorProduct.commContinuousAddMonoidHom B ⊗ 𝔸_K^f ≃ 𝔸_K^f ⊗ B as topological additive groups
396. NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul left multiplication and right multiplication by a unit have the same Haar character on B ⊗ 𝔸_K^f
397. MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_diagonal A diagonal matrix scales addHaar with its determinant
398. MeasureTheory.Matrix.TransvectionStruct.measurePreserving A transvection preserves addHaar on ι → F
399. MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_matrix_pi Haar measure scaling on (ι → F) for continuous linear equivalences generated by a matrix
400. MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_pi Haar measure scaling for linear maps on (ι → F)
401. MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming [SecondCountableTopology F]
402. MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming [SecondCountableTopology F]
403. MeasureTheory._root_.ContinuousLinearEquiv.mulLeft Multiplication on the left by a unit of an F-algebra which is a topological ring, is a continuous F-linear homeomorphism
404. MeasureTheory._root_.ContinuousLinearEquiv.mulRight Multiplication on the right by a unit of an F-algebra which is a topological ring, is a continuous F-linear homeomorphism
405. MeasureTheory.ringHaarChar_padic The distributive Haar character of the action of ℚ_[p]ˣ on ℚ_[p] is the usual p-adic norm
406. MeasureTheory.ringHaarChar_padicInt The distributive Haar character of the action of ℤ_[p]ˣ on ℤ_[p] is the constant 1
407. MeasureTheory.ringHaarChar_real The distributive Haar character of the action of ℝˣ on ℝ is the usual norm
408. MeasureTheory.ringHaarChar_complex The distributive Haar character of the action of ℂˣ on ℂ is the usual norm squared
409. MeasureTheory.ringHaarChar Documented declaration: ringHaarChar
410. MeasureTheory.ringHaarChar_eq_ringHaarChar_of_continuousAlgEquiv Transport ringHaarChar across a continuous ℤ-algebra equivalence (in place of continuous ring equivalences since we don't have them)
411. MeasureTheory.ringHaarCharKer The kernel of the ringHaarChar : Rˣ → ℝ≥0, namely the units of a locally compact topological ring such that left multiplication by them does not change additive Haar measure
412. MeasureTheory.ringHaarChar_prod Documented declaration: ringHaarChar_prod
413. Padic.unitBallPositiveCompact The unit ball as a compact set with nonempty interior
414. PadicInt.volume_coe https://github.com/ImperialCollegeLondon/FLT/issues/278
415. MeasureTheory._root_.QuotientGroup.isUnimodularGroup The quotient of a Hausdorff second countable unimodular group by a central normal closed subgroup is still unimodular
416. TensorProduct.RightActions.Algebra.TensorProduct.comm The A-algebra isomorphism A ⊗ B = B ⊗ A, available in the TensorProduct.RightActions scope
417. TensorProduct.RightActions.Module.TensorProduct.comm The A-module isomorphism A ⊗ M = M ⊗ A, available in the TensorProduct.RightActions scope
418. TensorProduct.RightActions.LinearMap.baseChange Base extension of an R-linear map V → W to an A-linear map V ⊗ A → W ⊗ A
419. TensorProduct.RightActions.LinearEquiv.baseChange Base extension of an R-linear iso V → W to an A-linear iso V ⊗ A → W ⊗ A
420. TensorProduct.RightActions.AlgebraMap.baseChange Base extension of an R-algebra map B → C to an A-linear map B ⊗ A → C ⊗ A
421. TensorProduct.RightActions.Algebra.TensorProduct.basis Right action version of Algebra.TensorProduct.basis -- base extension of a basis over a tensor product
422. Algebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq_aux A key induction step of exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq
423. Algebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq' A less universe polymorphic version of exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq
424. WeierstrassCurve.torsion_flat_of_good_reduction Documented declaration: torsion_flat_of_good_reduction
425. WeierstrassCurve.resultant_Φ_ΨSq The resultant of the division polynomials Φ n (taken with degree n²) and ΨSq n (taken with degree n² - 1) is ±Δ ^ ((n⁴ - n²)/6)
426. WeierstrassCurve.isCoprime_Φ_ΨSq Documented declaration: isCoprime_Φ_ΨSq
427. WeierstrassCurve.torsion_unramified_of_good_reduction Documented declaration: torsion_unramified_of_good_reduction
428. WeierstrassCurve.quadraticTwistOf Documented declaration: quadraticTwistOf
429. WeierstrassCurve.quadraticTwistOf_map The quadratic twist commutes with a ring homomorphism f (in particular with base change): (E.quadraticTwistOf t n).map f = (E.map f).quadraticTwistOf (f t) (f n)
430. WeierstrassCurve.kappa_quadraticTwistOf The node-polynomial constant κ = 54 b₆ - 3 b₂ b₄ + a₂ c₄ of the quadratic twist by (t, n) in terms of that of E: κ_W = D³ κ - D² n a₁² c₄ where D = t² - 4n
431. WeierstrassCurve.exists_smul_eq_quadraticTwistOf_quadraticTwistOf Documented declaration: exists_smul_eq_quadraticTwistOf_quadraticTwistOf
432. WeierstrassCurve.exists_smul_quadraticTwistOf_eq Documented declaration: exists_smul_quadraticTwistOf_eq
433. WeierstrassCurve.quadraticTwistBy The quadratic twist of a Weierstrass curve E over K by an element θ of an extension L/K: the twist WeierstrassCurve.quadraticTwistOf by the trace and norm of θ
434. WeierstrassCurve.exists_smul_quadraticTwistBy_eq The quadratic twist by a generator θ of a separable quadratic extension L/K depends on the choice of θ only up to isomorphism over K: all generators give isomorphic twists
435. WeierstrassCurve.quadraticTwist Documented declaration: quadraticTwist
436. WeierstrassCurve.baseChange_c₄_ne_zero If j(E) ≠ 0 then c₄ ≠ 0, also after base change to a field extension
437. WeierstrassCurve.baseChange_c₆_ne_zero If j(E) ≠ 1728 then c₆ ≠ 0, also after base change to a field extension
438. WeierstrassCurve.exists_smul_quadraticTwist_eq_quadraticTwistBy The quadratic twist of E by L/K is isomorphic over K to the twist by any given generator θ ∈ L ∖ K: the arbitrary choice made in its definition is harmless
439. WeierstrassCurve.exists_smul_baseChange_and_map_eq Documented declaration: exists_smul_baseChange_and_map_eq
440. WeierstrassCurve.exists_smul_quadraticTwist_baseChange_eq The quadratic twist becomes isomorphic to E after base change to L
441. WeierstrassCurve.exists_smul_quadraticTwist_quadraticTwist_eq Twisting twice by the same quadratic extension gives back E, up to K-isomorphism
442. WeierstrassCurve.quadraticTwist_of_two_ne_zero The classical formula for the quadratic twist away from characteristic 2
443. WeierstrassCurve.quadraticTwistVarChange A choice of change of variables over L carrying E to its quadratic twist Eᴸ
444. WeierstrassCurve.quadraticTwistVarChange_map The defining cocycle of the quadratic twist
445. WeierstrassCurve.j_quadraticTwist Twisting does not change the j-invariant, since the curves become isomorphic over L
446. WeierstrassCurve.not_exists_smul_quadraticTwist_eq If j(E) ∉ {0, 1728} (so that the only automorphisms of E are ±1) then the quadratic twist is not isomorphic to E over K: twisting by L/K is a nontrivial operation
447. WeierstrassCurve.exists_smul_eq_or_exists_smul_eq_quadraticTwist Documented declaration: exists_smul_eq_or_exists_smul_eq_quadraticTwist
448. WeierstrassCurve.quadraticTwistVarChange_baseChange_map Documented declaration: quadraticTwistVarChange_baseChange_map
449. WeierstrassCurve.quadraticTwistPointEquiv The isomorphism Eᴸ(M) ≅ E(M) on M-points, for any field M in a tower K ⊆ L ⊆ M: the base change to M of a choice of isomorphism between Eᴸ and E over L
450. WeierstrassCurve.quadraticTwistPointEquiv_map Documented declaration: quadraticTwistPointEquiv_map
451. WeierstrassCurve.quadraticTwistPointEquiv_map_of_not_fixed Documented declaration: quadraticTwistPointEquiv_map_of_not_fixed
452. WeierstrassCurve.quadraticTwistPointEquiv_galois Twisting the Galois action
453. WeierstrassCurve.quadraticTwistPointEquiv_conj Special case of quadraticTwistPointEquiv_galois over M = L itself: the isomorphism φ : Eᴸ(L) ≅ E(L) intertwines the action of the nontrivial element σ ∈ Gal(L/K) with -σ
454. WeierstrassCurve.exists_quadraticTwistPointEquiv_baseChange_eq_iff Documented declaration: exists_quadraticTwistPointEquiv_baseChange_eq_iff
455. WeierstrassCurve.nodePoly_quadraticTwistOf_map_splits_iff Twisting flips the square class (residue characteristic ≠ 2)
456. WeierstrassCurve.baseChange_integralModel_quadraticTwistOf Documented declaration: baseChange_integralModel_quadraticTwistOf
457. WeierstrassCurve.Δ_baseChange_quadraticTwistOf_ne_zero The base change of the twisted integral model has nonzero discriminant: its Δ is (t'² - 4n')⁶ · Δ (Δ_quadraticTwistOf), and both factors are nonzero
458. WeierstrassCurve.hasMultiplicativeReduction_baseChange_quadraticTwistOf The twist by a unit discriminant keeps multiplicative reduction
459. WeierstrassCurve.notMem_range_algebraMap_of_residue_notMem Documented declaration: notMem_range_algebraMap_of_residue_notMem
460. WeierstrassCurve.nodePoly_map_root_relations Documented declaration: nodePoly_map_root_relations
461. WeierstrassCurve.residue_c₄_mul_residue_eq_neg_c₆ Documented declaration: residue_c₄_mul_residue_eq_neg_c₆
462. WeierstrassCurve.nodePoly_quadraticTwistOf_map_splits_of_residue_of_two_eq_zero Documented declaration: nodePoly_quadraticTwistOf_map_splits_of_residue_of_two_eq_zero
463. WeierstrassCurve.nodePoly_quadraticTwistOf_map_splits_of_residue Documented declaration: nodePoly_quadraticTwistOf_map_splits_of_residue
464. WeierstrassCurve.hasSplitMultiplicativeReduction_quadraticTwistOf_of_residue Documented declaration: hasSplitMultiplicativeReduction_quadraticTwistOf_of_residue
465. WeierstrassCurve.exists_quadraticTwist_hasSplitMultiplicativeReduction Documented declaration: exists_quadraticTwist_hasSplitMultiplicativeReduction
466. ValuativeExtension.integerMap Documented declaration: integerMap
467. ValuativeExtension.integerMap_coe integerMap is the algebra map on underlying elements
468. ValuativeExtension.algebraMap_integerMap Documented declaration: algebraMap_integerMap
469. ValuativeExtension.residueMap The induced map of residue fields 𝒪[k]/𝓂[k] →+* 𝒪[l]/𝓂[l], from the local homomorphism integerMap
470. WeierstrassCurve.integralModel_baseChange_map The integral model of the base change is the base change of the integral model
471. WeierstrassCurve.valuation_c₄_baseChange_eq_one The c₄ of the base change has adic valuation 1
472. WeierstrassCurve.valuation_Δ_baseChange_lt_one The discriminant of the base change has adic valuation < 1
473. WeierstrassCurve.isMinimal_baseChange Documented declaration: isMinimal_baseChange
474. WeierstrassCurve.hasMultiplicativeReduction_baseChange Documented declaration: hasMultiplicativeReduction_baseChange
475. WeierstrassCurve.hasSplitMultiplicativeReduction_baseChange Base change along a valuative extension preserves split multiplicative reduction: the residue field only grows, and a split quadratic stays split under any ring map
476. WeierstrassCurve.tateA₄ The coefficient a₄(q) = -5s₃(q) of the Tate curve, where sₖ(q) = ∑_{n≥1} nᵏqⁿ/(1-qⁿ) (Silverman, ATAEC V.3)
477. WeierstrassCurve.tateA₆ Documented declaration: tateA₆
478. WeierstrassCurve.tateCurve The Tate curve E_q : y² + xy = x³ + a₄(q)x + a₆(q) (Silverman, ATAEC V.3)
479. WeierstrassCurve.tateCurveEquiv Tate's uniformisation of the Tate curve E_q, given by the explicit power series x = X(u, q), y = Y(u, q) of Silverman, ATAEC V.3
480. WeierstrassCurve.valuation_tateParameter_eq The Tate parameter of j has valuation exactly |j|⁻¹: the leading term j⁻¹ of the inverse series q = j⁻¹ + 744j⁻² + ⋯ dominates ultrametrically
481. WeierstrassCurve.valuation_Δ_lt_one An elliptic curve over k with bad (here multiplicative) reduction has discriminant of valuation less than 1: the discriminant of the integral model lies in the maximal ideal
482. WeierstrassCurve.valuation_c₄_eq_one An elliptic curve over k with multiplicative reduction has c₄ of valuation exactly 1: c₄ of the integral model is a unit of 𝒪[k]
483. WeierstrassCurve.valuation_Δ_ne_zero The discriminant of an elliptic curve has nonzero valuation
484. WeierstrassCurve.valuation_j_eq An elliptic curve over k with multiplicative reduction has |j| = |c₄|³/|Δ| = |Δ|⁻¹
485. WeierstrassCurve.one_lt_valuation_j Documented declaration: one_lt_valuation_j
486. WeierstrassCurve.q Documented declaration: q
487. WeierstrassCurve.valuation_q_lt_one The Tate parameter has norm less than 1
488. WeierstrassCurve.qUnit The Tate parameter as an element of kˣ
489. WeierstrassCurve.tateEquiv Tate's uniformization theorem: if E/k is an elliptic curve with split multiplicative reduction then E(k) is isomorphic to kˣ/⟨q⟩
490. WeierstrassCurve.exists_variableChange_tateCurve Documented declaration: exists_variableChange_tateCurve
491. WeierstrassCurve.tateA₄_eq_evalInt Documented declaration: tateA₄_eq_evalInt
492. WeierstrassCurve.tateA₆_eq_evalInt The Lambert series rearrangement for tateA₆, as for tateA₄_eq_evalInt; the bookkeeping of the exact division by 12 uses 12 ∣ 5d³ + 7d⁵ termwise
493. WeierstrassCurve.tateCurve_baseChange Documented declaration: tateCurve_baseChange
494. WeierstrassCurve.tateParameter_map The Tate parameter series commutes with valuative extensions: it is the evaluation of an integral power series at j⁻¹, so this is a direct instance of evalInt_map
495. WeierstrassCurve.qUnitSepClosure The image of the Tate parameter in a separable closure Ω of k, as a unit
496. WeierstrassCurve.tateEquivSepClosure Tate's uniformisation over a separable closure Ω of k: the union of the uniformisations of the E(l) over the finite subextensions l/k of Ω
497. WeierstrassCurve.tatePoint The point of E(Ω) corresponding to a unit x ∈ Ωˣ under Tate's uniformisation
498. WeierstrassCurve.tatePoint_galois Galois equivariance of the uniformisation over Ω: no continuity hypothesis is needed this time, since Ω/k is algebraic
499. WeierstrassCurve.tatePoint_mem_torsionBy_of_mem_rootsOfUnity N-th roots of unity give N-torsion points of E under Tate's uniformisation
500. WeierstrassCurve.tatePoint_mem_torsionBy_of_pow_eq N-th roots of the Tate parameter give N-torsion points of E under Tate's uniformisation
501. WeierstrassCurve.weilPairing_tatePoint weilPairing and tateEquiv/tateEquivSepClosure are all currently sorryed data, each pinned down mathematically only up to a sign
502. TateCurve.a₄Formal The formal a₄-series a₄(q) = -5s₃(q) ∈ ℤ⟦q⟧ of the Tate curve: the integral version of WeierstrassCurve.tateA₄
503. TateCurve.a₆Formal The formal a₆-series a₆(q) = -(5s₃(q) + 7s₅(q))/12 ∈ ℤ⟦q⟧ of the Tate curve: the integral version of WeierstrassCurve.tateA₆
504. TateCurve.hasSum_geometric_succ The geometric series over a nonarchimedean local field: for |x| < 1, x + x² + x³ + ⋯ = x/(1 - x)
505. TateCurve.tsum_lambert The Lambert series rearrangement over a nonarchimedean local field: for any integer coefficients c and |q| < 1, ∑_{m≥1} c(m)qᵐ/(1 - qᵐ) = ∑_{N≥1} (∑_{d ∣ N} c(d))qᴺ
506. TateCurve.tsum_lambert_eq_evalInt Documented declaration: tsum_lambert_eq_evalInt
507. TateCurve.valuation_evalInt_sub_sum_le Quantitative tail bound: the evaluation of an integral power series on the open unit disc is within |q|^N of its N-th partial sum
508. TateCurve.valuation_algebraMap_lt_one A valuative extension maps the open unit disc into the open unit disc: the induced map of value groups (ValuativeExtension.mapValueGroupWithZero) is strictly monotone
509. TateCurve.evalInt_map Documented declaration: evalInt_map
510. TateCurve.s The power series sₖ = ∑_{n ≥ 1} σₖ(n)qⁿ ∈ ℚ(u)⟦q⟧ (where σₖ(n) is the sum of the kth powers of the positive divisors of n)
511. TateCurve.a₄ The coefficient a₄ = -5s₃ = -5q - 45q² - ⋯ of the Tate curve y² + xy = x³ + a₄x + a₆
512. TateCurve.a₆ The coefficient a₆ = -(5s₃ + 7s₅)/12 = -q - 23q² - ⋯ of the Tate curve y² + xy = x³ + a₄x + a₆
513. TateCurve.X The power series X(u,q) = u/(1-u)² + ∑_{n ≥ 1} (∑_{d ∣ n} d(uᵈ + u⁻ᵈ - 2)) qⁿ ∈ ℚ(u)⟦q⟧, the x-coordinate of the uniformisation kˣ/qᶻ ≃ E_q(k) of the Tate curve
514. TateCurve.Y Documented declaration: Y
515. TateCurve.Blueprint.e e z = exp (2πiz)
516. TateCurve.Blueprint.periodPair The pair of periods (τ, 1), for τ not real
517. TateCurve.Blueprint.hasSum_lattice_prod Transport of a HasSum over the lattice Λ_τ = ℤτ + ℤ along the reindexing ℤ × ℤ ≃ Λ_τ, (n, m) ↦ nτ + m
518. TateCurve.Blueprint.sAn The convergent power series sₖ(q) = ∑_{n ≥ 1} σₖ(n)qⁿ, for ‖q‖ < 1 (junk value otherwise); the evaluation of the formal series TateCurve.s k at q
519. TateCurve.Blueprint.XAn The analytic function Xₐ(u, q) = ∑_{n : ℤ} qⁿu/(1 - qⁿu)² - 2s₁(q), defined for 0 < ‖q‖ < 1 and u ∉ qᶻ (junk value otherwise)
520. TateCurve.Blueprint.YAn The analytic function Yₐ(u, q) = ∑_{n : ℤ} (qⁿu)²/(1 - qⁿu)³ + s₁(q), defined for 0 < ‖q‖ < 1 and u ∉ qᶻ (junk value otherwise)
521. TateCurve.Blueprint.hasSum_choose_two_mul_geometric The Lambert-type sum ∑_{n ≥ 0} (n choose 2)rⁿ = r²/(1 - r)³ for ‖r‖ < 1, by shifting the index in ∑' n, ((n + 2).choose 2) * rⁿ = 1/(1 - r)³
522. TateCurve.Blueprint.tsum_sq_mul_geometric_of_norm_lt_one Documented declaration: tsum_sq_mul_geometric_of_norm_lt_one
523. TateCurve.Blueprint.sum_int_inv_pow_succ Row sum, exponent k + 1 ≥ 2, with the Lambert sum in series form: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻⁽ᵏ⁺¹⁾ = ((-2πi)ᵏ⁺¹/k!) ∑_{d ≥ 0} dᵏ e(w)ᵈ
524. TateCurve.Blueprint.sum_int_inv_sq Row sum, exponent 2: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻² = (2πi)² e(w)/(1 - e(w))²
525. TateCurve.Blueprint.sum_int_inv_cube Documented declaration: sum_int_inv_cube
526. TateCurve.Blueprint.summable_int_inv_pow ∑_{m : ℤ} (w + m)⁻ᵏ converges (absolutely) for every w and k ≥ 2
527. TateCurve.Blueprint.tsum_int_inv_pow_neg Evenness of the row sum under w ↦ -w, for even exponents
528. TateCurve.Blueprint.tsum_int_inv_pow_neg_odd Oddness of the row sum under w ↦ -w, for odd exponents
529. TateCurve.Blueprint.hasSum_int_inv_pow The Basel-type sums over ℤ: ∑_{m : ℤ} m⁻ᵏ = 2ζ(k) for even k ≥ 2 (the m = 0 term is junk 0)
530. TateCurve.Blueprint.inv_div_one_sub_inv_sq The rational-function identity v⁻¹/(1 - v⁻¹)² = v/(1 - v)² (true for v ≠ 0, including v = 1 where both sides are junk 0)
531. TateCurve.Blueprint.norm_pow_div_one_sub_pow_le Norm bound for vʲ/(1 - v)ᵏ when ‖v‖ ≤ a < 1
532. TateCurve.Blueprint.summable_aux' If ‖x‖ < 1 and ‖xy‖ < 1 then ∑_{n ≥ 1} (xⁿy)ʲ/(1 - xⁿy)ᵏ converges for j ≥ 1 (the terms decay geometrically)
533. TateCurve.Blueprint.summable_aux If ‖x‖ < 1 and ‖xy‖ < 1 then ∑_{n ≥ 1} xⁿy/(1 - xⁿy)² converges (the terms decay geometrically)
534. TateCurve.Blueprint.sum_int_inv_sq' Extension of sum_int_inv_sq to w in the lower half plane, using the evenness of w ↦ ∑_m (w + m)⁻² and the invariance of v/(1-v)² under v ↦ v⁻¹
535. TateCurve.Blueprint.hasSum_int_inv_sq The Basel problem over ℤ: ∑_{m : ℤ} m⁻² = π²/3 (the m = 0 term is junk 0)
536. TateCurve.Blueprint.tsum_pnat_of_zero Dropping a vanishing 0th term: ∑'_{n : ℕ+} g n = ∑'_{n : ℕ} g n when g 0 = 0 (true without summability hypotheses, since both sides are junk simultaneously)
537. TateCurve.Blueprint.tsum_pnat_coe_mul_geometric The Lambert sum over ℕ+: ∑_{c ≥ 1} c xᶜ = x/(1 - x)² for ‖x‖ < 1
538. TateCurve.Blueprint.tsum_V_nat The Lambert-to-divisor-sum rearrangement: ∑_{n ≥ 0} qⁿ/(1 - qⁿ)² = ∑_{N ≥ 1} σ₁(N)qᴺ (the n = 0 term is junk 0)
539. TateCurve.Blueprint.tsum_corr_int The corrector sum over ℤ: ∑_{n : ℤ} qⁿ/(1 - qⁿ)² = 2∑_{N ≥ 1} σ₁(N)qᴺ (the n = 0 term is junk 0, and n ↔ -n are equal)
540. TateCurve.Blueprint.norm_mul_lt_one ‖qu‖ < 1 when ‖q‖ < ‖u‖ < 1
541. TateCurve.Blueprint.norm_mul_inv_lt_one ‖qu⁻¹‖ < 1 when 0 < ‖q‖ < ‖u‖
542. TateCurve.Blueprint.zpow_neg_natCast_mul The substitution v ↦ v⁻¹ on v = qⁿu⁻¹ produces q⁻ⁿu
543. TateCurve.Blueprint.summable_V Summability of the series defining XAn, for 0 < ‖q‖ < ‖u‖ < 1
544. TateCurve.Blueprint.im_sub_int_mul_ne_zero For 0 < im z < im τ, every row z - nτ avoids the real axis
545. TateCurve.Blueprint.corrector_row_eval Documented declaration: corrector_row_eval
546. TateCurve.Blueprint.weierstrassP_q_expansion Documented declaration: weierstrassP_q_expansion
547. TateCurve.Blueprint.inv_sq_div_one_sub_inv_cube The rational-function identity (v⁻¹)²/(1 - v⁻¹)³ = -(v/(1 - v)³) for v ≠ 0
548. TateCurve.Blueprint.inv_mul_one_add_inv_div_one_sub_inv_cube The rational-function identity v⁻¹(1 + v⁻¹)/(1 - v⁻¹)³ = -(v(1 + v)/(1 - v)³) for v ≠ 0: the function on the right-hand side of sum_int_inv_cube is odd under v ↦ v⁻¹
549. TateCurve.Blueprint.div_sq_add_two_mul_div_cube Documented declaration: div_sq_add_two_mul_div_cube
550. TateCurve.Blueprint.sum_int_inv_cube' Extension of sum_int_inv_cube to w in the lower half plane
551. TateCurve.Blueprint.summable_V₂ Summability of the series defining YAn, for 0 < ‖q‖ < ‖u‖ < 1
552. TateCurve.Blueprint.derivWeierstrassP_q_expansion The q-expansion of ℘' (Silverman, Advanced topics, Theorem I.6.2): under the hypotheses of weierstrassP_q_expansion, ℘'(z; Λ_τ) = (2πi)³ (Xₐ(e z, e τ) + 2Yₐ(e z, e τ))
553. TateCurve.Blueprint.sum_int_inv_fourth Row sum, exponent 4: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻⁴ = (2πi)⁴/6 ⬝ ∑_{d ≥ 1} d³e(w)ᵈ
554. TateCurve.Blueprint.hasSum_int_inv_fourth The Basel-type sum over ℤ in weight 4: ∑_{m : ℤ} m⁻⁴ = π⁴/45
555. TateCurve.Blueprint.not_summable_natCast_pow ∑ dᵏ diverges; used to see that the Lambert series contributes junk 0 in the n = 0 row
556. TateCurve.Blueprint.tsum_natCast_pow_mul_one The junk value of the Lambert series in the row n = 0: ∑_{d ≥ 0} dʲ ⬝ 1ᵈ = 0, since the series diverges
557. TateCurve.Blueprint.tsum_tsum_pow_eq_sAn The divisor-sum rearrangement ∑_{n ≥ 0} ∑_{d ≥ 0} dʲ q^{nd} = sⱼ(q) for ‖q‖ < 1 and j ≠ 0 (the row n = 0 is junk 0, and the terms d = 0 vanish)
558. TateCurve.Blueprint.tsum_int_lambert_natAbs The two-tailed version: ∑_{n : ℤ} ∑_{d ≥ 0} dʲ q^{|n|d} = 2sⱼ(q) for ‖q‖ < 1 and j ≠ 0, given summability of the rows
559. TateCurve.Blueprint.row_eval_ne_zero Rows n ≠ 0 of an even-weight lattice sum, via a row-sum identity hrow valid on the upper half plane (evenness reduces n < 0 to n > 0)
560. TateCurve.Blueprint.G_q_expansion Documented declaration: G_q_expansion
561. TateCurve.Blueprint.g₂_q_expansion The q-expansion of g₂ (Silverman, Advanced topics, Theorem I.7.1): g₂(Λ_τ) = (2πi)⁴/12 ⬝ (1 + 240s₃(q))
562. TateCurve.Blueprint.riemannZeta_six The value ζ(6) = π⁶/945 (companion to Mathlib's riemannZeta_four)
563. TateCurve.Blueprint.sum_int_inv_sixth Row sum, exponent 6: for w in the upper half plane, ∑_{m : ℤ} (w + m)⁻⁶ = (2πi)⁶/120 ⬝ ∑_{d ≥ 1} d⁵e(w)ᵈ
564. TateCurve.Blueprint.hasSum_int_inv_sixth The Basel-type sum over ℤ in weight 6: ∑_{m : ℤ} m⁻⁶ = 2ζ(6) = 2π⁶/945
565. TateCurve.Blueprint.g₃_q_expansion The q-expansion of g₃ (Silverman, Advanced topics, Theorem I.7.1): g₃(Λ_τ) = -(2πi)⁶/216 ⬝ (1 - 504s₅(q))
566. TateCurve.Blueprint.analytic_weierstrass The analytic form of the main theorem (Silverman, Advanced topics, Theorem V.1.1(a)): for 0 < ‖q‖ < ‖u‖ < 1, Yₐ² + XₐYₐ = Xₐ³ - 5s₃(q)Xₐ - (5s₃(q) + 7s₅(q))/12
567. TateCurve.Blueprint.evalAt Evaluation of a rational function in ℚ(u) at a complex number, with junk value 0 at the (finitely many) poles
568. TateCurve.Blueprint.evalAtHom For transcendental u, evaluation at u is a ring homomorphism ℚ(u) →+* ℂ (there are no poles to produce junk values)
569. TateCurve.Blueprint.tsum_int_decomp Splitting a summable ℤ-indexed sum into the term at 0 and the two tails
570. TateCurve.Blueprint.norm_pow_mul_lt_one If ‖q‖ < 1 and ‖q * y‖ < 1 then ‖qⁿy‖ < 1 for every n ≥ 1
571. TateCurve.Blueprint.summable_coeff_prod Geometric-decay summability of the double series ∑ a(m)yᵐq^{nm}, for any coefficients of at most quadratic growth
572. TateCurve.Blueprint.hasSum_prod_pnat A summable double series over ℕ+ × ℕ+ has sum the iterated sum of its rows
573. TateCurve.Blueprint.hasSum_prod_lambert Fubini for the Lambert-type double series with coefficients a of at most quadratic growth, whose rows sum in closed form to g (qⁿy)
574. TateCurve.Blueprint.hasSum_divisor_collect Collecting a double series ∑_{n,m} g(m)x^{nm} by powers of x: the coefficient of x^N is the divisor sum ∑_{d ∣ N} g d
575. TateCurve.Blueprint.hasSum_prodC The y = 1 double series, with the divisor sums already recognised as s₁
576. TateCurve.Blueprint.hasSum_X_eval Documented declaration: hasSum_X_eval
577. TateCurve.Blueprint.hasSum_Y_eval Rearrangement for Y: for 0 < ‖q‖ < ‖u‖ < 1 with u transcendental, the coefficients of the formal series TateCurve.Y evaluated at u sum to Yₐ(u, q)
578. TateCurve.Blueprint.hasSum_a₄_eval The coefficients of the formal series a₄ evaluated at any u sum to -5s₃(q) for ‖q‖ < 1
579. TateCurve.Blueprint.hasSum_a₆_eval The coefficients of the formal series a₆ evaluated at any u sum to -(5s₃(q) + 7s₅(q))/12 for ‖q‖ < 1
580. TateCurve.Blueprint.eq_zero_of_forall_hasSum_zero Documented declaration: eq_zero_of_forall_hasSum_zero
581. TateCurve.weierstrass_equation The point (X(u,q), Y(u,q)) satisfies the Weierstrass equation y² + xy = x³ + a₄x + a₆ of the Tate curve, as an identity in ℚ(u)⟦q⟧
582. TateCurve.sInt The formal series sₖ(q) = ∑_{n≥1} σₖ(n)qⁿ ∈ ℤ⟦q⟧ (integer-coefficient version of TateCurve.s; recall σₖ(0) = 0)
583. TateCurve.c₄Formal The formal c₄-series c₄(q) = 1 + 240s₃(q) = 1 + 240q + 2160q² + ⋯ ∈ ℤ⟦q⟧ of the Tate curve: the q-expansion of the Eisenstein series E₄
584. TateCurve.ΔFormal The formal discriminant Δ(q) = q∏_{n≥1}(1 - qⁿ)²⁴ ∈ ℤ⟦q⟧ of the Tate curve: the q-expansion of the modular discriminant, ∑ τ(n)qⁿ with τ Ramanujan's tau
585. TateCurve.jInv The formal series 1/j = Δ(q)/c₄(q)³ = q - 744q² + 356652q³ - ⋯ ∈ ℤ⟦q⟧: the reciprocal of the j-invariant of the Tate curve
586. TateCurve.jInvReverse Documented declaration: jInvReverse
587. TateCurve.subst_jInvReverse The defining property of jInvReverse: ψ(jInv(q)) = q as formal power series
588. TateCurve.jInv_subst_jInvReverse The composition in the other order: jInv(ψ(w)) = w as formal power series
589. TateCurve.evalInt The evaluation ∑ₙ Fₙqⁿ ∈ k of an integral power series F ∈ ℤ⟦X⟧ at a point q of a topological field (junk value if the series does not converge)
590. TateCurve.summable_of_valuation_le_pow Documented declaration: summable_of_valuation_le_pow
591. TateCurve.tendsto_pow_nhds_zero Powers of an element of the open unit disc tend to zero
592. TateCurve.summable_evalInt Documented declaration: summable_evalInt
593. TateCurve.valuation_evalInt_le_pow Documented declaration: valuation_evalInt_le_pow
594. TateCurve.valuation_evalInt_eq Documented declaration: valuation_evalInt_eq
595. TateCurve.evalInt_mul Evaluation of integral power series at a point of the open unit disc is multiplicative
596. TateCurve.evalInt_pow Evaluation of integral power series at a point of the open unit disc respects powers: iterated evalInt_mul
597. WeierstrassCurve.tateParameter Documented declaration: tateParameter
598. WeierstrassCurve.torsion_rank_two then the n-torsion of E(k) is free rank 2 over ℤ/nℤ
599. WeierstrassCurve.weilPairing The Weil pairing on the n-torsion of an elliptic curve E over a separably closed field k, a bilinear pairing with values in the n-th roots of unity of k
600. Dickson.K An algebraic closure K p of the finite field 𝔽_p = ZMod p
601. Dickson.PGL The projective general linear group PGL₂(K p), i.e. GL₂(K p) modulo its centre
602. Dickson.PSL The projective special linear group PSL₂(K p)
603. OddRep.isIrreducible_iff_isAbsolutelyIrreducible Proposition 1.2 / Theorem 1.3
604. _root_.LinearEquiv.mulLeft The F-linear equivalence on an F-algebra induced by left multiplication by a unit
605. _root_.LinearEquiv.mulRight The F-linear equivalence on an F-algebra induced by right multiplication by a unit
606. AlgEquiv.apply_mem_range_algebraMap_iff An algebra isomorphism identifies the images of the base ring: e x lies in the image of F if and only if x does
607. SemialgHom Let φ : R →+* S be a ring homomorphism, let A be an R-algebra and let B be an S-algebra
608. SemialgHomClass SemialgHomClass F φ A B states that F is a type of φ-semialgebra homomorphisms from A to B, where A is an R-algebra, B is an S-algebra and φ : R →+* S
609. SemialgHomClass.toSemialgHom Turn an element of F which satisfies SemialgHomClass F φ A B to a SemialgHom
610. SemialgHom.comp The composition of two semi-algebra maps
611. AlgHom.toSemialgHom An algebra map defines a semi-algebra map using RingHom.id
612. RingHom.toSemialgHom Promote a ring hom f : A →+* B which is φ-semilinear to a semi-algebra map
613. SemialgHom.compAlgHom The composition (B →ₛₐ[ψ] C) ∘ (A →ₐ[S] B) → A →ₛₐ[ψ] C` of a semi-algebra map with an algebra map to give a semi-algebra map
614. SemialgHom.prod The product of two semi-algebra maps on the same domain
615. SemialgHom.prodMap The product of two semi-algebra maps on separate domains
616. SemialgHom.restrictScalars Restrict the scalars of semialgebra map f : A →ₛₐ[ψ] B where ψ : R' →ₛₐ[φ] S', to φ : R →+* S
617. Pi.semialgHom A family of semialgebra homomorphisms g i : A →ₛₐ[φ] f i defines a single semialgebra homomorphism A →ₛₐ[φ] (i : I) → f i to the product algebra
618. Pi.semialgHomPi Documented declaration: semialgHomPi
619. AlgEquiv.piCongrFiberwise Let f : α → β be a function on index types
620. IsBiscalar If f : A → B where A and B are both R- and S-modules, then IsBiscalar R S f asserts that f satisfies the linear scalar property for both R and S
621. LinearMap.changeScalars Documented declaration: changeScalars
622. LinearEquiv.changeScalars Documented declaration: changeScalars
623. AlgEquiv.extendScalars Documented declaration: extendScalars
624. AlgHom.changeScalars Produces an S'-linear algebra map from an S-linear algebra map f : A →ₐ[S] B which also has scalars S'
625. AlgEquiv.changeScalars Produces an S'-linear algebra isomorphism from an S-linear algebra isomorphism f : A ≃ₐ[S] B which also has scalars S'
626. TopModuleCat.linHom The internal hom of two topological modules: the space of continuous linear maps A →L[k] B carrying the topology induced from the compact-open topology on C(A, B)
627. TopModuleCat.linHomMap Pre- and post-composition induce a morphism between the internal homs of topological modules
628. TopModuleCat.homOfBilinear Bundle a bilinear pairing with jointly continuous uncurried form into a morphism to the internal hom
629. TopModuleCat.cokerDesc The universal property of the concrete quotient TopModuleCat.coker: a morphism killing the range descends to the quotient
630. TopModuleCat.cokerCongr Cokernels of morphisms identified under an isomorphism of the targets are isomorphic
631. TopModuleCat.cokerDescCLM Descend a continuous linear map along cokernel projections on both sides
632. TopModuleCat.continuous_cokerDescCLM_uncurry The descended family of continuous linear maps has jointly continuous uncurried form
633. TopModuleCat.cokerDescBilinear Descend a bilinear pairing, bundled as a morphism into the internal hom, along cokernel projections in all three slots
634. HomologicalComplex.cyclesIsoKer The cycles of a complex of topological modules, identified with the kernel of the differential carrying the subspace topology
635. HomologicalComplex.homologyIsoCoker The homology of a complex of topological modules, identified with the quotient of the cycles by the boundaries, carrying the quotient topology
636. MulAction.FixedPoints If M acts on A then FixedPoints M A is the type of elements of A which are fixed elementwise by all of M
637. AddAction.FixedPoints If M acts on A then FixedPoints M A is the type of elements of A which are fixed elementwise by all of M
638. MulAction.FixedPoints.addMonoid TODO: I could use FixedPoints.addSubmonoid + coercion to addMonoid, but Is my nsmul better?
639. MulAction.FixedPoints.smul_neg should be in mathlib; current version assumes M a monoid but same proof
640. MulActionHom.compLeftAlgHom Composing MulActionHom on the left as an AlgHom
641. MulActionHom.toFunAlgHom The coercion from MulActionHom to functions as an AlgHom
642. MulActionHom.evalAlgHom Evaluating a MulActionHom is an AlgHom, bundled as a MulActionHom
643. AlgHom.evalMulActionHom Evaluating a AlgHom is an MulActionHom, bundled as a AlgHom
644. CochainComplex.prev_nat The predecessor function of the cochain complex shape on ℕ is truncated subtraction
645. IsDirectLimit IsDirectLimit f g states that P is the direct limit of the system (M i, f i j hij)
646. IsDirectLimit.preimageIndex Documented declaration: preimageIndex
647. IsDirectLimit.preimage Given an element p : P in the direct limit, preimage f g p returns an element of M (preimageIndex f g p) that maps to p under g (preimageIndex f g p)
648. IsDirectLimit.lift Construct a map P₁ → P₂ from a direct limit by sending each element to its preimage in some component M i and applying g₂ i
649. IsDirectLimit.Equiv Any two direct limits of the same directed system are isomorphic
650. IsDirectLimit.Module.lift The universal property of the direct limit: define a linear map from the direct limit by giving a compatible family of linear maps from the components
651. IsDirectLimit.Module.linearEquiv Any two direct limits of the same directed system are isomorphic
652. IsQuaternionAlgebra IsQuaternionAlgebra F D says that D is a quaternion algebra over the field F, i.e. a four-dimensional central simple F-algebra
653. IsQuaternionAlgebra.IsTotallyDefinite Documented declaration: IsTotallyDefinite
654. Subring.toSubmodule If S is a subring of R, then S can be viewed as an S-submodule of R
655. Equiv.module' Transfer Module across an Equiv, where the additive structure on the source is itself obtained by transporting the one on the target back along the equivalence
656. Equiv.linearEquiv' Documented declaration: linearEquiv'
657. Polynomial.derivative_quadratic The derivative of the quadratic a X² + b X + c is 2 a X + b
658. Polynomial.sq_derivative_quadratic_sub_mul The Bézout-type identity (P')² - 4 a · P = C (b² - 4 a c) for the quadratic P = a X² + b X + c: the discriminant is an explicit combination of P and its derivative
659. Polynomial.separable_quadratic_iff A quadratic polynomial a X² + b X + c (with a ≠ 0) over a field is separable exactly when its discriminant b² - 4 a c is nonzero
660. Polynomial.splits_quadratic_iff_exists_root A quadratic a X² + b X + c (a ≠ 0) over a field splits exactly when it has a root (Splits.of_natDegree_le_two_of_isRoot)
661. Polynomial.splits_quadratic_iff Documented declaration: splits_quadratic_iff
662. Polynomial.splits_quadratic_iff_of_two_eq_zero Documented declaration: splits_quadratic_iff_of_two_eq_zero
663. Polynomial.Splits.of_natDegree_le_two_of_isRoot A polynomial of degree at most 2 over a field splits as soon as it has a root: the root splits off a linear factor and the cofactor is linear
664. WeierstrassCurve.Affine.variableChange_negY_ne The image of a pair of points under the change of variables satisfies the y₁ = -y₂ degeneracy condition (negY) only if the original pair does
665. WeierstrassCurve.Affine.variableChange_equation A point (x, y) lies on C • W if and only if (u²x + r, u³y + u²sx + t) lies on W: the change of variables scales the Weierstrass polynomial by u⁶
666. WeierstrassCurve.Affine.Point.mapVariableChangeFun The underlying map (C • W).Point → W.Point of the change of variables, sending 0 to 0 and (x, y) to (u²x + r, u³y + u²sx + t)
667. WeierstrassCurve.Affine.Point.equivOfEq Transport of the affine point group along an equality of Weierstrass curves
668. WeierstrassCurve.Affine.Point.mapVariableChange The group homomorphism (C • W).Point →+ W.Point induced by the admissible change of variables (x, y) ↦ (u²x + r, u³y + u²sx + t)
669. WeierstrassCurve.Affine.Point.equivVariableChange The group isomorphism (C • W).Point ≃+ W.Point induced by the admissible change of variables (x, y) ↦ (u²x + r, u³y + u²sx + t), with inverse coming from C⁻¹
670. WeierstrassCurve.r_eq_zero_of_u_eq_one An automorphism C of E with C.u = 1 has no x-translation: C.r = 0
671. WeierstrassCurve.eq_one_or_eq_negVariableChange_of_u_eq_one An automorphism C of E with C.u = 1 is either the identity or negVariableChange E
672. WeierstrassCurve.u_eq_one_or_eq_neg_one The u-coefficient of an automorphism C of E (with c₄, c₆ ≠ 0) satisfies u² = 1: the c₄ and c₆ laws give u⁴ = u⁶ = 1
673. WeierstrassCurve.eq_one_or_eq_negVariableChange_of_smul_eq_of_c₄_ne_zero If c₄ ≠ 0 and c₆ ≠ 0 then the only admissible changes of variables fixing E are 1 and negVariableChange E
674. WeierstrassCurve.eq_one_or_eq_negVariableChange_of_smul_eq If j(E) ∉ {0, 1728} then the only admissible changes of variables fixing E are 1 and negVariableChange E; that is, Aut(E) = {±1}
675. WeierstrassCurve.autGroup The automorphism group of a Weierstrass curve E over a field: the admissible changes of variables fixing E, i.e. the stabiliser of E under the action of VariableChange K
676. WeierstrassCurve.autGroupMulEquiv Aut(E) ≅ ℤ/2 for j(E) ∉ {0, 1728}
677. WeierstrassCurve.exists_baseChange_eq_of_map_eq Galois descent for changes of variables
678. WeierstrassCurve.exists_baseChange_point_eq_of_map_eq Galois descent for points
679. WeierstrassCurve.nodePoly Documented declaration: nodePoly
680. WeierstrassCurve.nodePoly_map The node polynomial base-changed along a ring homomorphism
681. WeierstrassCurve.map_nodePoly Documented declaration: map_nodePoly
682. WeierstrassCurve.aeval_root_nodePoly_map The root of the (base-changed) node polynomial satisfies its defining quadratic relation
683. WeierstrassCurve.nodePoly_map_eq_quadratic The reduced node polynomial, presented as a quadratic with an additive constant term — the form consumed by the quadratic separability and splitting criteria
684. WeierstrassCurve.map_splitPolynomial_discrim The image of the discriminant identity splitPolynomial_discrim under a ring homomorphism, in the shape produced by the quadratic criteria applied to nodePoly_map_eq_quadratic
685. WeierstrassCurve.nodePoly_smul Documented declaration: nodePoly_smul
686. WeierstrassCurve.nodePoly_map_splits_smul_iff Invariance of the node polynomial's splitting under change of variables
687. WeierstrassCurve.nodePoly_map_splits_iff_isSquare Split criterion (residue characteristic ≠ 2)
688. WeierstrassCurve.nodePoly_map_splits_iff_of_two_eq_zero Split criterion (residue characteristic 2)
689. WeierstrassCurve.integralModel_baseChange The integral model of the base change to K of an integral Weierstrass curve W over R is W itself (integral models are unique, as R → K is injective)
690. WeierstrassCurve.HasSplitMultiplicativeReduction.baseChange_smul Split multiplicative reduction is a change-of-variables invariant
691. WeierstrassCurve.residue_integralModel_c₄_ne_zero Multiplicative reduction forces c₄ of the integral model to be a unit: its residue is nonzero (valuation c₄ = 1 means c₄ ∉ maximalIdeal)
692. WeierstrassCurve.residue_integralModel_Δ_eq_zero Multiplicative reduction (bad reduction) means the discriminant of the integral model has zero residue
693. WeierstrassCurve.residue_integralModel_c₆_ne_zero Multiplicative reduction forces c₆ of the integral model to be a unit too: from 1728 Δ = c₄³ - c₆² and Δ ≡ 0, c₆² ≡ c₄³ ≢ 0
694. WeierstrassCurve.not_splits_nodePoly_of_not_hasSplit Nonsplit multiplicative reduction means precisely that the node polynomial of the integral model does not split over the residue field
695. WeierstrassCurve.natDegree_nodePoly_map The node polynomial over the residue field is a genuine quadratic (leading coefficient c₄ is a unit)
696. WeierstrassCurve.irreducible_nodePoly_map For nonsplit multiplicative reduction, the node polynomial is irreducible over the residue field: it is a quadratic that does not split, so (over a field) it has no linear factors
697. WeierstrassCurve.separable_nodePoly_map Documented declaration: separable_nodePoly_map
698. WeierstrassCurve.isMinimal_of_valuation_c₄_eq_one Minimality criterion
699. WeierstrassCurve.valuation_Δ_aux_smul_le For a minimal Weierstrass model W, no integral change of variables increases the valuation of the discriminant
700. WeierstrassCurve.valuation_Δ_eq_of_isMinimal_smul Two minimal Weierstrass models related by a change of variables have the same valuation of the discriminant
701. WeierstrassCurve.valuation_u_eq_one_of_isMinimal_smul Documented declaration: valuation_u_eq_one_of_isMinimal_smul
702. WeierstrassCurve.exists_variableChange_baseChange_eq_of_smul_eq Documented declaration: exists_variableChange_baseChange_eq_of_smul_eq
703. WeierstrassCurve.HasSplitMultiplicativeReduction.of_isMinimal_smul Split multiplicative reduction is an isomorphism invariant of minimal models
704. WeierstrassCurve.VariableChange.instDecidableEq Two admissible changes of variables agree iff their four coefficients do; this makes equality of changes of variables decidable over a commutative ring with decidable equality
705. WeierstrassCurve.negVariableChange The automorphism [-1] : (x, y) ↦ (x, -y - a₁x - a₃) of a Weierstrass curve, as an admissible change of variables ⟨-1, 0, -a₁, -a₃⟩
706. WeierstrassCurve.negVariableChange_map Base change commutes with the negation automorphism: mapping [-1] on W through a ring homomorphism φ gives [-1] on W.map φ
707. WeierstrassCurve.negVariableChange_ne_one Documented declaration: negVariableChange_ne_one
708. WeierstrassCurve.negVariableChange_baseChange_map The automorphism [-1] of E over L is defined over K, hence fixed by the Galois action: its components -1, 0, -a₁, -a₃ all lie in K
709. WeierstrassCurve.baseChange_smul_baseChange Base change commutes with the action of changes of variables
710. WeierstrassCurve.smul_eq_of_baseChange_smul_eq A relation Cᴸ • Vᴸ = Wᴸ between base changes, with C defined over K, descends to C • V = W over K
711. WeierstrassCurve.map_smul_baseChange_eq The Galois conjugate of an L-isomorphism between base-changed curves is again one
712. WeierstrassCurve.splitPolynomial_discrim The discriminant of the node's tangent polynomial c₄ T² + a₁ c₄ T - (54 b₆ - 3 b₂ b₄ + a₂ c₄) (the quadratic controlling split multiplicative reduction) equals -c₄ c₆
713. WeierstrassCurve.a₁_ne_zero_or_a₃_ne_zero_of_two_eq_zero In characteristic 2, an elliptic curve has a₁ ≠ 0 or a₃ ≠ 0: otherwise a₁ = a₃ = 0 makes the partial derivative ∂/∂y = 2y + a₁x + a₃ vanish identically, so Δ = 0
714. WeierstrassCurve.c₆_eq_zero_iff_j_eq_1728 c₆(E) = 0 if and only if j(E) = 1728, by the relation 1728·Δ = c₄³ - c₆²
715. Int.eq_floor The file this was destined for (Mathlib.Data.Real.Archimedean) no longer exists -- it was moved to Mathlib.Algebra.Order.Archimedean.Real.Basic
716. forall_apply_algebraMap_iff_restrictNormal_eq_one For a normal subextension K ⊆ L ⊆ M, a K-automorphism σ of M fixes L pointwise if and only if its restriction to L (AlgEquiv.restrictNormal) is the identity
717. Algebra.IsQuadraticExtension.card_algEquiv A separable quadratic extension has exactly two automorphisms
718. Algebra.IsQuadraticExtension.exists_algEquiv_ne_one A separable quadratic extension has a nontrivial automorphism
719. Algebra.IsQuadraticExtension.algEquiv_eq_one_or_eq The only automorphisms of a separable quadratic extension are the identity and any given nontrivial automorphism
720. Algebra.IsQuadraticExtension.algEquiv_mul_self The nontrivial automorphism of a separable quadratic extension is an involution
721. Algebra.IsQuadraticExtension.mem_range_algebraMap_of_apply_eq An element fixed by a nontrivial automorphism — hence, Gal(L/K) having order two, by all of Gal(L/K) — lies in the base field
722. Algebra.IsQuadraticExtension.univ_algEquiv The automorphism group of a separable quadratic extension consists of the identity and one nontrivial element
723. Algebra.IsQuadraticExtension.algEquiv_apply_ne The nontrivial automorphism of a separable quadratic extension moves every element lying outside the base field
724. Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq The nontrivial automorphism of a separable quadratic extension sends a square root α ∉ K of an element of K to -α
725. quadraticCharacter The quadratic character of Aut(M/K) attached to a separable quadratic subextension K ⊆ L ⊆ M: it sends σ to 1 if σ fixes L pointwise, and to -1 otherwise
726. quadraticCharacter_surjective Documented declaration: quadraticCharacter_surjective
727. MulAction.etaleSubalgebraEquiv Documented declaration: etaleSubalgebraEquiv
728. Polynomial.exists_monic_dvd_dvd_derivative_of_not_separable A nonzero polynomial over a field that is not separable has a monic common divisor of positive degree with its derivative, namely its normalized gcd with the derivative
729. Algebra.IsSeparable.of_isSeparable_of_adjoin_eq_top A field extension generated by a single separable element is separable
730. DoubleCoset.map Mapping double cosets across MonoidHoms
731. DoubleCoset.quotientEquiv Mapping double cosets across MulEquivs
732. DoubleCoset.mulRightEquiv The isomorphism H\G/K ≃ H\G/g⁻¹Kg sending HaK to H(ag)(g⁻¹Kg)
733. DoubleCoset.ofLeft The projection G/K → H\G/K
734. DoubleCoset.ofRight The projection H\G → H\G/K
735. DoubleCoset.toMapIdPreimage_preimage Given K₁ ≤ K₂, the map f : H\G/K₁ → H\G/K₂ is surjective
736. DoubleCoset.ncard_toMapIdPreimage_preimage Given K₁ ≤ K₂, the map f : H\G/K₁ → H\G/K₂ is surjective
737. DoubleCoset.σ An arbitrary section of G → H＼G／K
738. DoubleCoset.σLeft An arbitrary choice of h such that h * σ(g) * K = g
739. DoubleCoset.σRight An arbitrary choice of k such that h * σ(g) * K = g
740. MulAction.homEquivProdFixedPoints Documented declaration: homEquivProdFixedPoints
741. MulAction.sigmaRangeQuotientStabilizer Documented declaration: sigmaRangeQuotientStabilizer
742. mulEquivMultiplicativeZModTwo Documented declaration: mulEquivMultiplicativeZModTwo
743. Countable.of_module_finite TODO upstream
744. Module.Finite.equivPi Choice of an R-linear isomorphism M ≃ R^(finrank R M) for a finite free module M over a ring R with the strong rank condition
745. TensorProduct.AlgebraTensorModule.finiteEquivPi Base change of Module.Finite.equivPi to an R-algebra N: the equivalence N ⊗[R] M ≃ₗ[N] Fin (finrank R M) → N
746. linearIndependent_one_of_notMem_range_algebraMap 1 and any element lying outside the base field are linearly independent over the base field
747. Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap A quadratic extension contains an element not in the base field
748. Algebra.IsQuadraticExtension.exists_eq_algebraMap_add_algebraMap_mul Any element of a quadratic extension L/K is a K-linear combination of 1 and a given generator θ, and the θ-coefficient is nonzero if the element also lies outside K
749. notMem_range_algebraMap_of_not_isSquare An element whose square is (the image of) a nonsquare of K lies outside K
750. Matrix.GeneralLinearGroup.diagonal The invertible diagonal matrix associated to a vector of units (the diagonal entries)
751. Matrix.GeneralLinearGroup.GL2.unipotent The unipotent matrix element !![1, t; 0, 1]
752. Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec The claim that a matrix is a product of transvections, a diagonal matrix, and more transvections
753. Matrix.TransvectionStruct.map Base change of a TransvectionStruct along a ring homomorphism
754. Matrix.diagonal_transvection_induction' Documented declaration: diagonal_transvection_induction'
755. Matrix.diagonal_transvection_induction_of_det_unit this proof is literally cut and pasted from mathlib with ≠ 0 changed to IsUnit and 𝕜 changed to R and addition of (hM : ExistsListTransvecMulDiagonalMulListTransvec M)
756. Pi.FiberwiseSMul A class encoding the product scalar multiplication of ∀ b : β, R b on ∀ a : α, M a that is determined by the fibers of a supplied function f : α → β on indices
757. LinearEquiv.piScalarPiCongrFiberwise Let f : α → β be a function on index types
758. LinearEquiv.piScalarPiComm Documented declaration: piScalarPiComm
759. Prod.IsProdSMul A class encoding the product scalar multiplication of R × S on M × N of the format x • y = (x.1 • y.1, x.2 • y.2)
760. RestrictedProduct.FiberwiseSMul Documented declaration: FiberwiseSMul
761. AlgHom.rTensor The base extension of an R-algebra homomorphism f : N → P to an f-semilinear map N ⊗[R] M → P ⊗[R] M
762. LinearEquiv.chooseBasisPiScalarRight The M-algebra isomorphism M ⊗ V ≃ₗ[M] (ι → M) coming from the canonical ι-indexed basis of a finite free R-module V
763. IsUnimodularGroup A group with topolgoy is a unimodular group if it is a locally compact topological group such that the modular character is trivial
764. modularCharacter_mul_relIndex_conjAct Documented declaration: modularCharacter_mul_relIndex_conjAct
765. relIndex_conjAct_eq If G is a unimodular group, and K₁, K₂ are compact open subgroups of G such that K₁ contains both K₁ and gK₁g⁻¹, then [K₂ : gK₁g⁻¹] = [K₂ : K₁]
766. relIndex_conjAct_inv_smul_self If G is a unimodular group, and K₁, K₂ are compact open subgroups of G such that K₁ contains both K₁ and gK₁g⁻¹, then [K₂ : gK₁g⁻¹] = [K₂ : K₁]
767. exists_bijOn_mk_image_mul_singleton_and_mk_image_mul_singleton_inv There exists a set of coset representatives βᵢ of UgU such that UgU = ⨆ βᵢgU and Ug⁻¹U = ⨆ βᵢ⁻¹g⁻¹U
768. MeasureTheory.Units.haarMeasure Given a locally compact topological ring R such that Rˣ → R is an open embedding
769. MeasureTheory.Units.haarMeasure_apply Can replace IsOpenUnits R + SecondCountableTopology R by PolishSpace R
770. MeasureTheory.Matrix.mopContinuousMulEquiv For any ring R, we have ring isomorphism Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose
771. MeasureTheory.Matrix.transposeContinuousMulEquiv For any ring R, we have ring isomorphism Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ given by transpose
772. TopologicalGroup.IsSES.not_injOn_of_inducedMeasure_gt A sufficiently large open subset of B cannot be a fundamental domain
773. NumberField.InfiniteAdeleRing.algEquivMixedSpace If K is a number field, this is the ℝ-linear iso between ∏_v|∞ K_v and ℝ^r × ℂ^s, with the usual notation
774. NumberField.InfiniteAdeleRing.continuousAlgEquivMixedSpace If K is a number field, this is the continuous ℝ-linear iso between ∏_v|∞ K_v and ℝ^r × ℂ^s, with the usual notation
775. Rat.infinitePlaceCompletionContinuousAlgEquiv The continuous ℤ-algebra isomorphism between Rat.infinitePlace.Completion and ℝ
776. PadicInt.smul_submodule_one_relIndex x • S has index ‖x‖⁻¹ in S, where S is the copy of ℤ_[p] inside ℚ_[p]
777. PadicInt.smul_submodule_one_isFiniteRelIndex x • S has finite in S, where S is the copy of ℤ_[p] inside ℚ_[p]
778. PadicInt.closure_nonZeroDivisors_padicInt Non-zero p-adic integers generate non-zero p-adic numbers as a group
779. Filter.cofinite.sets.countable TODO upstream
780. Representation.glMapOfBasis Documented declaration: glMapOfBasis
781. Representation.baseChange Base change of a representation along a commutative R-algebra R': extends ρ : G → GL(V) to R' ⊗[R] V
782. ContRepresentation.linHom Documented declaration: linHom
783. ContRepresentation.continuous_pair_of_discrete When the source module of an intertwining map into an internal hom is discrete, its uncurried pairing is automatically jointly continuous
784. TopRep.iHom The internal hom of two topological representations: the topological representation on the space of continuous linear maps A →L[k] B, with G acting by conjugation
785. ContRepresentation.resolutionCLM Documented declaration: resolutionCLM
786. ContRepresentation.resolutionCLM_conj Conjugating u : M2 →L[k] M3 by the representations corresponds to conjugating resolutionCLM u by the coinduced actions on the resolutions
787. ContRepresentation.resolutionXCast Transport between two levels of the standard resolution along an equality of indices, as a continuous linear map
788. ContRepresentation.d_hom_zero The zeroth differential of the standard resolution is the constant-function embedding
789. ContRepresentation.d_hom_succ_apply The pointwise formula for the differentials of the standard resolution
790. ContRepresentation.resolutionCLM_comp_d The differentials of the standard resolutions are compatible with the functorial extension resolutionCLM of a continuous linear map
791. ContRepresentation.invariantsObjIHom Documented declaration: invariantsObjIHom
792. ContRepresentation.eqToHom_iHom_apply Applying an eqToHom reindexing morphism between internal homs of resolution levels to elements is transport along the index equality
793. ContinuousCohomology._root_.TopRep.homogeneousCochains.d_comp_d_apply Applying two consecutive differentials of the homogeneous cochain complex gives zero
794. ContinuousCohomology.bdryKer The coboundary map into the kernel model: the differential corestricted to the cocycles of the next degree
795. ContinuousCohomology.toCycles_comp_cyclesIsoKer_hom Under the identification of the cycles with the kernel model, toCycles becomes the corestricted differential bdryKer
796. ContinuousCohomology.cohomologyIsoQuot Continuous cohomology identified with the quotient of the kernel model of the cocycles by the coboundaries, carrying the quotient topology
797. ContRepresentation.cupSucc Documented declaration: cupSucc
798. ContRepresentation.continuous_cupSucc_uncurry The uncurried pairing of cupSucc F hF is again jointly continuous, so cupSucc can be iterated
799. ContRepresentation.cupZeroSuccAux The pairing resolutionX (of ρ2) n × M1 → resolutionX (of ρ3) n underlying the cup product, sending (y, v) to resolutionCLM (f v) n y, as a continuous map
800. ContRepresentation.cupZeroSucc Documented declaration: cupZeroSucc
801. ContRepresentation.continuous_cupZeroSucc_uncurry The uncurried pairing of cupZeroSucc f hp n is jointly continuous, so cupSucc applies to it
802. ContRepresentation.cupPair Documented declaration: cupPair
803. ContRepresentation.cupComplex Documented declaration: cupComplex
804. ContRepresentation.cupZeroSucc_const_apply Cupping with a constant 0-cochain acts through the functorial extension of f v
805. ContRepresentation.cupPair_d_comm The Leibniz rule for the cup product pairing on the levels of the standard resolutions: d (σ ∪ τ) = (d σ) ∪ τ + (-1) ^ m • (σ ∪ d τ)
806. ContinuousCohomology.cupCochain The cup product pairing on homogeneous cochains, obtained from the cup product pairing cupComplex on the coinduced resolutions by taking invariants
807. ContinuousCohomology.cupCochain_coe The value of the cup product of two homogeneous cochains, as an element of the resolution
808. ContinuousCohomology.cupCochain_zero_apply cupCochain vanishes when its first argument is zero
809. ContinuousCohomology.d_cupCochain_eq_zero The cup product of two cocycles is a cocycle
810. ContinuousCohomology.cupKerCLM For a fixed cocycle σ, cupping with σ restricts to a continuous linear map between the kernels of the differentials on homogeneous cochains
811. ContinuousCohomology.cupCochain_d_comp_d The cup product with a doubly-applied differential vanishes
812. ContinuousCohomology.d_cup_d The cup product of two coboundaries is a coboundary: (d σ) ∪ (d τ) = d (σ ∪ d τ)
813. ContinuousCohomology.d_cupCochain_of_d_eq_zero Cupping a coboundary with a cocycle gives a coboundary
814. ContinuousCohomology.cupCochain_d_of_d_eq_zero Cupping a cocycle with a coboundary gives a coboundary, up to the sign (-1) ^ m
815. ContinuousCohomology.continuous_cupKerCLM_uncurry The cup product pairing on the kernels of the differentials is jointly continuous
816. ContinuousCohomology.cupKerHom The cup product bundled as a morphism from the kernel of the differential into the internal hom of the kernel models
817. ContinuousCohomology.cupCocyclesAux The cup product of two cocycles, as a cocycle: by the Leibniz rule cup_d_comm, the differential of σ ∪ τ vanishes when d σ = 0 and d τ = 0
818. ContinuousCohomology.cupCocycles The cup product pairing on the cycles of the homogeneous cochain complexes, transporting cupKerHom along the identification cyclesIsoKer of the cycles with the kernel models
819. ContinuousCohomology.cokerπ_cupKerCLM_bdryKer_left Cupping a coboundary with a cocycle dies in the quotient by the coboundaries
820. ContinuousCohomology.cokerπ_cupKerCLM_bdryKer_right Cupping a cocycle with a coboundary dies in the quotient by the coboundaries
821. ContinuousCohomology.cup Documented declaration: cup
822. AdjoinRoot.map_comp_mk Reduction along f : A →+* B descends to AdjoinRoot: the square A[X] → B[X] → B[X]/(q) = A[X] → A[X]/(p) → B[X]/(q) commutes when q = p.map f
823. AdjoinRoot.finrank_eq_natDegree The simple extension F[X]/(q) by a root of an irreducible q has degree natDegree q
824. AdjoinRoot.natDegree_minpoly_root The minimal polynomial of root q has the same degree as the irreducible q
825. AdjoinRoot.eq_zero_of_mul_root_add_eq_zero Documented declaration: eq_zero_of_mul_root_add_eq_zero
826. AdjoinRoot.root_notMem_range_algebraMap The root of an irreducible polynomial of degree at least 2 does not lie in the base field
827. IsDedekindDomain.HeightOneSpectrum.liesOver_under A height one prime of B lies over its pullback to A
828. IsDedekindDomain.HeightOneSpectrum.adicCompletion.algEquiv adicCompletion.equiv as a K-algebra isomorphism onto the underlying completion
829. IsDedekindDomain.FiniteAdeleRing.structureMap The structure map Π 𝒪ᵥ → 𝔸ᶠ as a ring hom
830. IsDedekindDomain.FiniteAdeleRing.integralAdeles The integral adele subring inside the finite adele ring
831. IsDedekindDomain.FiniteAdeleRing.mk Constructor for FiniteAdeleRing R K
832. IsDedekindDomain.FiniteAdeleRing.evalAlgebraMap The K-algebra map 𝔸_K^f → Kᵥ from the finite adele ring of K to a completion
833. IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap The continuous K-algebra map 𝔸_K^f → Kᵥ from the finite adele ring of K to a completion
834. IsDedekindDomain.FiniteAdeleRing.singleLinearMap The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles
835. IsDedekindDomain.FiniteAdeleRing.singleMulHom The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles
836. IsDedekindDomain.FiniteAdeleRing.singleContinuousLinearMap The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles
837. IsDedekindDomain.FiniteAdeleRing.localIdempotent localIdempotent R K p is the finite adele which is 1 at p and 0 elsewhere
838. IsDedekindDomain.FiniteAdeleRing.singleContinuousAlgebraMap_comp_evalContinuousLinearMap The composite 𝔸_K^f --(eval)--> Kᵥ --(single)--> 𝔸_K^f is multiplication by the local idempotent at v
839. RingEquiv.heightOneSpectrumComap Pulling back elements of HeightOneSpectrum along a ring isomorphism
840. RingEquiv.heightOneSpectrum The bijection HeightOneSpectrum A ≃ HeightOneSpectrum B induced by a ring isomorphism between A and B
841. Nat.Prime.toHeightOneSpectrumInt The element of HeightOneSpectrum ℤ associated to a prime number
842. Nat.Prime.toHeightOneSpectrumRingOfIntegersRat The element of HeightOneSpectrum (𝓞 ℚ) associated to a prime number
843. IsDiscreteValuationRing.injective_of_not_maximalIdeal_le_ker Documented declaration: injective_of_not_maximalIdeal_le_ker
844. Field.exists_monic_irreducible_adjoinRoot_algEquiv Documented declaration: exists_monic_irreducible_adjoinRoot_algEquiv
845. IsLocalRing.exists_monic_map_residue_eq A monic polynomial over the residue field of a local ring lifts to a monic polynomial of the same degree over the ring
846. IsLocalRing.of_isMaximal_map_maximalIdeal Documented declaration: of_isMaximal_map_maximalIdeal
847. AdjoinRoot.residueFieldEquiv If S = A[X]/(P) is local with maximal ideal 𝔪_A · S, then its residue field is (A/𝔪_A)[X]/(P mod 𝔪_A)
848. AdjoinRoot.isSeparable_root The root of an irreducible separable polynomial q is a separable element of F[X]/(q): its minimal polynomial is q up to a unit
849. AdjoinRoot.isSeparable_of_separable The simple extension F[X]/(q) by a root of an irreducible separable polynomial is separable
850. AdjoinRoot.isMaximal_map_maximalIdeal If the reduction of P modulo the maximal ideal of a local ring A is irreducible, then 𝔪_A · A[X]/(P) is a maximal ideal: the quotient by it is the field (A/𝔪_A)[X]/(P̄)
851. AdjoinRoot.isDiscreteValuationRing_of_irreducible_map_residue Documented declaration: isDiscreteValuationRing_of_irreducible_map_residue
852. AdjoinRoot.exists_nonZeroDivisor_mul_eq_algebraMap Documented declaration: exists_nonZeroDivisor_mul_eq_algebraMap
853. AdjoinRoot.isFractionRing_map Documented declaration: isFractionRing_map
854. Polynomial.Monic.separable_map_algebraMap_of_separable_map_residue A monic polynomial over a discrete valuation ring R whose reduction to the residue field is separable stays separable over the fraction field K
855. IsLocalization.leftModuleTensorEquiv If A is a localization of R, tensoring two A-modules over A is the same as tensoring them over R
856. Algebra.IsQuadraticExtension.algebraMap_trace_eq_add In a separable quadratic extension, the trace of x is x + σx, where σ is the nontrivial automorphism
857. Algebra.IsQuadraticExtension.algebraMap_norm_eq_mul In a separable quadratic extension, the norm of x is x * σx, where σ is the nontrivial automorphism
858. Algebra.IsQuadraticExtension.trace_algebraMap_add_algebraMap_mul The trace of b + aθ in a separable quadratic extension is a·tr(θ) + 2b
859. Algebra.IsQuadraticExtension.norm_algebraMap_add_algebraMap_mul The norm of b + aθ in a separable quadratic extension is b² + ab·tr(θ) + a²·N(θ)
860. Algebra.IsQuadraticExtension.discrim_ne_zero Documented declaration: discrim_ne_zero
861. Algebra.IsQuadraticExtension.trace_eq_zero_of_sq_eq A square root α ∉ K of an element of K has trace 0: the nontrivial automorphism sends α to -α (Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq)
862. Algebra.IsQuadraticExtension.norm_eq_neg_of_sq_eq A square root α ∉ K of d ∈ K has norm -d: the nontrivial automorphism sends α to -α (Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq)
863. sq_sub_trace_mul_self_add_norm Rank-2 Cayley–Hamilton
864. norm_quotient_mk Norm and the residue field
865. sq_sub_trace_mul_self_add_norm_residue Documented declaration: sq_sub_trace_mul_self_add_norm_residue
866. Polynomial.Monic.exists_monic_map_eq_of_monic_dvd_map Documented declaration: exists_monic_map_eq_of_monic_dvd_map
867. Ideal.ramificationIdx_mul_inertiaDeg_eq_finrank_of_isLocalRing The fundamental identity e * f = [S : R] for a local ring S, finite over a Dedekind domain R, and p a nonzero maximal ideal of R
868. exists_unramified_extension_of_residueField Unramified lifting, arbitrary degree
869. exists_algebraMap_unit_eq_of_valuation_eq_one An element of the fraction field of a discrete valuation ring with valuation 1 is the image of a unit
870. ValuativeRel.valuation_natCast_le_one Naturals have valuation at most 1: they lie in the integer subring (valuation R).integer of the valuation
871. ValuativeRel.valuation_intCast_le_one Integers have valuation at most 1: they lie in the integer subring (valuation R).integer of the valuation
872. ValuativeRel.exists_pow_valuation_lt Powers of an element of the open unit disc become arbitrarily small
873. ValuativeRel.adicValuation_lt_one_iff Documented declaration: adicValuation_lt_one_iff
874. ValuativeRel.adicValuation_eq_one_iff On an integral element, the adic valuation attached to the maximal ideal of 𝒪[K] equals 1 exactly when the canonical valuation does: both detect unitality in 𝒪[K]
875. ValuativeExtension.valuation_algebraMap_le_one A valuative extension maps the closed unit disc into the closed unit disc; in other words, algebraMap A B maps the ring of integers 𝒪[A] into 𝒪[B]
876. ValuativeExtension.valuation_algebraMap_lt_one A valuative extension maps the open unit disc into the open unit disc; in other words, algebraMap A B maps the maximal ideal of 𝒪[A] into that of 𝒪[B]
877. ValuativeExtension.valuation_algebraMap_eq_one A valuative extension maps the unit circle into the unit circle; in other words, algebraMap A B maps units of 𝒪[A] to units of 𝒪[B]
878. ContinuousSemialgHom A SemialgHom (i.e., ψ such that ψ (r • a) = φ r • ψ a for some φ : R →+* S) that is also continuous
879. ContinuousSemialgHomClass ContinuousSemialgHomClass F φ A B states that F is the type of continuous semi-algebra maps from A to B with respect to φ
880. ContinuousSemialgHom._root_.ContinuousSemialgHomClass.toContinuousSemialgHom Turn an element of F which satisfies ContinuousSemialgHomClass F φ A B to a ContinuousSemialgHom
881. ContinuousSemialgHom.prod The product of two continuous semi-algebra isomorphisms on the same domain
882. ContinuousSemialgHom.prodMap the product of two continuous semi-algebra isomorphisms on different domains
883. ContinuousAlgEquiv.changeScalars Produces an S'-linear continuous algebra isomorphism from a continuous algebra isomorphism f : A ≃A[S] B which also has scalars S'
884. ContinuousAddEquiv.toIntContinuousLinearEquiv Reinterpret a continuous additive equivalence between additive groups as a continuous ℤ-linear equivalence
885. ContinuousAddEquiv.quotientPi For a finite family of topological additive groups G i and subgroups p i ≤ G i, the canonical continuous additive isomorphism (∏ i, G i) ⧸ (∏ i, p i) ≃ₜ+ ∏ i, (G i ⧸ p i)
886. ContinuousMulEquiv.mapUnits Any ContinuousMulEquiv induces a ContinuousMulEquiv on units
887. ContinuousSMulDiscrete ContinuousSMulDiscrete G M means that the action G × M → M is continuous when M is given the discrete topology (See continuousSMulDiscrete_iff)
888. ContinuousLinearEquiv.piScalarPiCongrFiberwise Let f : α → β be a function on index types
889. ContinuousLinearEquiv.piScalarPiComm Documented declaration: piScalarPiComm
890. Matrix.toContinuousLinearEquiv Given M : Matrix ι ι F, b : Module.Basis ι F V and h : M.det ≠ 0, this is the continuous linear equivalence arising from Matrix.toLinearEquiv b M (Ne.isUnit h)
891. ModuleTopology.iff should be in Mathlib
892. IsModuleTopology.isTopologicalModule making this into an instance causes timeouts in the BaseChange file :-/
893. IsModuleTopology._root_.moduleTopology.trans If S is an R-algebra, finite as an R-module, with the module topology, then the S-module topology on an S-module coincides with the R-module topology
894. IsModuleTopology.of_continuous_isOpenMap_algebraMap An R-algebra S has the R-module topology if the embedding R →+* S is continuous and open
895. IsModuleTopology.continuousLinearEquiv Documented declaration: continuousLinearEquiv
896. IsModuleTopology.continuousLinearEquivOfIsBiscalar A linear equivalence e : A ≃ₗ[S] B which also has scalars S', with A and B both having the S'-module topology, is automatically continuous
897. IsModuleTopology.continuousAlgEquivOfIsBiscalar An algebra isomorphism e : A →ₐ[S] B which also has scalars S', with A and B both having the S'-module topology, is automatically continuous
898. IsModuleTopology.continuousAlgEquivOfAlgEquiv An algebra isomorphism between two topological algebras over R with the R-module topology is automatically an algebra homeomorphism
899. IsModuleTopology.t2Space A free module with the module topology over a T2Space ring is a T2Space
900. IsModuleTopology.t2Space' A vector space with the module topology over a T2Space ring is a T2Space
901. IsModuleTopology._root_.Prod.instFinite_leftAlgebra A is a finite (A × B)-module
902. IsModuleTopology._root_.Prod.instFinite_rightAlgebra B is a finite (A × B)-module
903. IsModuleTopology.Prod.instLeftAlgebra A has the (A × B)-module topology
904. IsModuleTopology.Prod.instRightAlgebra B has the (A × B)-module topology
905. IsModuleTopology.Prod.instLeftModule If M has the A-module topology, then it also has the (A × B)-module topology
906. IsModuleTopology.Prod.instRightModule If N has the B-module topology, then it also has the (A × B)-module topology
907. IsModuleTopology.instProd' If M has the A-module topology and N has the B-module topology then M × N has the (A × B)-module topology
908. IsModuleTopology.locallyCompactSpaceOfFinite can't be an instance because typeclass inference can't find R
909. Submodule.Quotient.continuousLinearEquiv A continuous R-linear equivalence e : G ≃L[R] H sending the submodule G' ≤ G onto H' ≤ H descends to a continuous R-linear equivalence G ⧸ G' ≃L[R] H ⧸ H'
910. Submodule.quotientPiContinuousLinearEquiv For a finite family of topological R-modules G i and submodules p i ≤ G i, the canonical continuous R-linear equivalence (∏ i, G i) ⧸ ∏ i, p i ≃L[R] ∏ i, G i ⧸ p i
911. ContinuousLinearEquiv.chooseBasisPiScalarRight Documented declaration: chooseBasisPiScalarRight
912. ContinuousLinearEquiv.chooseBasisPiScalarRight' Documented declaration: chooseBasisPiScalarRight'
913. ContinuousLinearMap.rTensor' The continuous R-linear map M ⊗[R] V → N ⊗[R] V induced by a continuous R-linear map M → N
914. induced_continuous_smul note: use convert not exact to ensure typeclass inference doesn't try to find topology on B
915. AbsoluteValue.lt_one_iff_of_lt_one_imp If v is a nontrivial absolute value, and w is another absolute value such that w x < 1 if v x < 1, then we must also have v x < 1 if w x < 1
916. AbsoluteValue.log_div_image_eq_singleton_of_le_one_iff If v and w are two real absolute values on F, v is non-trivial, and v x < 1 if and only if w x < 1, then log (v a) / log (w a) is constant for all a ∈ K
917. AbsoluteValue.eq_rpow_iff_lt_one_iff Let v and w be two real absolute values on F, where v is non-trivial
918. AbsoluteValue.exists_lt_one_one_le_of_ne_rpow If v is non-trivial and v = w ^ t for some t > 0, then we can find an a ∈ F such that v a < 1 while 1 ≤ w a
919. AbsoluteValue.exists_one_lt_lt_one_of_ne_rpow If v and w are two non-trivial absolute values such that v = w ^ t for some t > 0, then we can find an a ∈ K such that 1 < v a while w a < 1
920. RestrictedProduct.mapAlongLinearMap Documented declaration: mapAlongLinearMap
921. RestrictedProduct.inclusionLinearMap Documented declaration: inclusionLinearMap
922. RestrictedProduct.SubmonoidClass.isProductAt A submonoid U of a resticted product of monoids is a product at i if U can be written as Uᵢ × Uⁱ with Uᵢ supported at the i'th component and Uⁱ supported away from i
923. RestrictedProduct.mem_coset_and_mulSupport_subset_of_isProductAt If U is a product at i and g is supported at i then UgU can be written as a disjoint union of cosets gᵢU with the gᵢ supported at i
924. RestrictedProduct.structureMapRingHom The structure map for a restricted product of ring
925. RestrictedProduct.structureSubring The subring ∏ i, A i inside Πʳ i, [R i, A i]_[𝓕]
926. Equiv.restrictedProductCongrRight The equivalence between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets
927. MulEquiv.restrictedProductUnits The isomorphism between the units of a restricted product of monoids, and the restricted product of the units of the monoids
928. RingEquiv.restrictedProductCongrRight The ring isomorphism between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets
929. LinearEquiv.restrictedProductCongrRight The LinearEquiv between restricted products built from LinearEquivs on the factors
930. Equiv.restrictedProductCongrLeft' The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters
931. Equiv.restrictedProductCongrLeft The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters
932. AddEquiv.restrictedProductCongrLeft' Documented declaration: restrictedProductCongrLeft'
933. AddEquiv.restrictedProductCongrLeft Documented declaration: restrictedProductCongrLeft
934. MulEquiv.restrictedProductCongrLeft' Documented declaration: restrictedProductCongrLeft'
935. MulEquiv.restrictedProductCongrLeft Documented declaration: restrictedProductCongrLeft
936. RingEquiv.restrictedProductCongrLeft' The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters
937. RingEquiv.restrictedProductCongrLeft The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters
938. LinearEquiv.restrictedProductCongrLeft' The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters
939. LinearEquiv.restrictedProductCongrLeft The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters
940. Equiv.restrictedProductCongr The equivalence between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors
941. AddEquiv.restrictedProductCongr The additive monoid isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors
942. MulEquiv.restrictedProductCongr Documented declaration: restrictedProductCongr
943. RingEquiv.restrictedProductCongr The ring isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors
944. LinearEquiv.restrictedProductCongr The linear isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors
945. Equiv.restrictedProductProd The bijection between a restricted product of binary products, and the binary product of the restricted products
946. Equiv.restrictedProductPi The bijection between a restricted product of finite products, and a finite product of restricted products
947. Equiv.restrictedProductMatrix The bijection between a restricted product of m x n matrices, and m x n matrices of restricted products
948. RestrictedProduct.flatten The canonical map from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set
949. RestrictedProduct.flattenEquiv The canonical bijection from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set
950. RestrictedProduct.flattenEquiv' The equivalence given by flatten when both restricted products are over the cofinite filter
951. RestrictedProduct.principalEquivProd The canonical isomorphism between Πʳ i, [R i, A i]_[𝓟 S] and (Π i ∈ S, R i) × (Π i ∉ S, A i)
952. RestrictedProduct.principalMulEquivProd Additive monoid equivalence of principalEquivProd
953. RestrictedProduct.principalLinearEquivProd Module equivalence version of principalEquivProd
954. RestrictedProduct.linearMapComponent Components of a linear map
955. RestrictedProduct.piSubringSubmodule If B i is subring of R i then (B i)^n is a B i-submodule of (R i)^n
956. RestrictedProduct._root_.LinearEquiv.restrictedProductPi Canonical linear equivalence between Π' R^n and (Π' R)^n
957. RestrictedProduct._root_.ContinuousLinearEquiv.restrictedProductPi Canonical continuous linear equivalence between Π' R^n and (Π' R)^n
958. Equiv.continuous_restrictedProductProd The forward direction of Equiv.restrictedProductProd is continuous with any filter, not just the cofinite one
959. Homeomorph.restrictedProductProd The homeomorphism between restricted product of binary products, and the binary projuct of the restricted products, when the products are with respect to open subsets
960. Equiv.continuous_restrictedProductPi The forward direction of Equiv.restrictedProductPi is continuous with any filter, not just the cofinite one
961. Homeomorph.restrictedProductPi The homeomorphism between a restricted product of finite products, and a finite product of restricted products, when the products are with respect to open subsets
962. Homeomorph.restrictedProductMatrix The homeomorphism between a restricted product of m x n matrices, and m x n matrices of restricted products, when the products are with respect to open sets
963. ContinuousMulEquiv.restrictedProductUnits Documented declaration: restrictedProductUnits
964. ContinuousMulEquiv.restrictedProductMatrix The monoid homeomorphism between a restricted product of n x n matrices, and n x n matrices of restricted products, when the products are with respect to open sets
965. ContinuousMulEquiv.restrictedProductMatrixUnits Documented declaration: restrictedProductMatrixUnits
966. RestrictedProduct.flattenHomeomorph The canonical homeomorphism from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set
967. RestrictedProduct.flattenHomeomorph' The homeomorphism given by flatten when both restricted products are over the cofinite filter and there's a topology on the factors
968. RestrictedProduct.mem_nhds_iff_of_principal An explicit condition for a set to be in the neighborhood of x : Πʳ i, [G i, C i]_[𝓟 T] in terms of a product of neighbourhoods on the factors
969. RestrictedProduct.mem_nhds_of_exists_nhds_of_cofinite A condition for a set to be a neighborhood in Πʳ i, [G i, C i], slightly weaker than the condition in mem_nhds_iff_of_cofinite
970. RestrictedProduct.mem_nhds_iff_of_cofinite The classical condition for a set to be a neighborhood in the restricted product
971. Homeomorph.restrictedProductPrincipal The canonical homeomorphism between a restricted product Πʳ i, [R i, A i]_[𝓟 J] over a principal filter, and the corresponding product (Π i : J, A i) × (Π i : Jᶜ, R i)
972. RestrictedProduct.singleContinuousAddMonoidHom The inclusion from a factor into the restricted product of topological additive groups, as a continuous group homomorphism
973. RestrictedProduct.evalContinuousAddMonoidHom The continuous additive projection from a restricted product of topological additive groups to a factor
974. UniformSpace.Completion.mapSemialgHom The semialgebra homomorphism Completion α →ₛₐ[f] Completion β induced from a continuous ring homomorphism f : α →+* β
975. ValuativeRel.integerBallIdeal Documented declaration: integerBallIdeal
976. Valued.WithZeroMulInt.finite_quotient_maximalIdeal_pow_of_finite_residueField Note: this is copied directly from the mathlib result Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField with a relaxation on some of the hypotheses on K
977. Valued.WithZeroMulInt.finite_cover_of_uniformity_basis Documented declaration: finite_cover_of_uniformity_basis
978. Valued.WithZeroMulInt.integer_compactSpace The ring of integers 𝒪[K] of a complete ℤᵐ⁰-valued field K with finite residue field is compact, whenever 𝒪[K] is a discrete valuation ring
979. TopologicalSpace.secondCountableTopology_of_countable_cover' find home and upstream
980. ContinuousMap.continuous_prodMk Documented declaration: continuous_prodMk
981. continuous_of_discreteTopology_snd A map on X × D with D discrete is continuous as soon as all its slices x ↦ g (x, d) are continuous
982. DenseRange.exists_matrix_det_ne_zero Let A : X → Matrix n n R be a parameterisation of a matrix ring with entries in a seminormed commutative ring R by a metric space X and let f : Y → X be dense
983. NumberField.AdeleRing.baseChange The canonical map from the adeles of K to the adeles of L
984. NumberField.AdeleRing.baseChangeAlgEquiv The L-algebra isomorphism L ⊗[K] 𝔸_K = 𝔸_L
985. NumberField.AdeleRing.baseChangeEquiv The L-algebra homeomorphism L ⊗[K] 𝔸 K = 𝔸 L
986. NumberField.AdeleRing.tensorProductEquivPi A continuous K-linear isomorphism L ⊗[K] 𝔸_K = (𝔸_K)ⁿ for n = [L:K]
987. NumberField.AdeleRing.piEquiv A continuous additive isomorphism (𝔸_K)ⁿ ≃ 𝔸_L for n = [L:K]
988. NumberField.AdeleRing.piQuotientEquiv A continuous additive isomorphism (𝔸_K / K)ⁿ = 𝔸_L / L where n = [L:K]
989. NumberField.AdeleRing.ModuleBaseChangeLinearEquiv V ⊗[K] 𝔸_K = V ⊗[L] 𝔸_L as L-modules for V an L-module and K ⊆ L number fields
990. NumberField.AdeleRing.ModuleBaseChangeContinuousLinearEquiv 𝔸_K ⊗[K] V = 𝔸_L ⊗[L] V as topological additive groups for V an L-module and K ⊆ L number fields
991. Rat.AdeleRing.fundamentalDomain The fundamental domain ℤ^ x [0,1) for 𝔸_ℚ ⧸ ℚ
992. FiniteAdeleRing.toAdicCompletion The canonical ring homomorphism from the finite adele ring to a nonarchimedean local factor
993. Rat.AdeleRing.mem_fundamentalDomain bleurgh
994. Rat.AdeleRing.fundamentalDomain_traversal Documented declaration: fundamentalDomain_traversal
995. NumberField.AdeleRing.baseChangeAdeleAlgHom The canonical 𝔸 K-algebra homomorphism (L ⊗_K 𝔸 K) → 𝔸 L induced by the maps from L and 𝔸 K into 𝔸 L
996. NumberField.AdeleRing.baseChangeAlgAdeleEquiv The canonical 𝔸_K-algebra isomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the base change map 𝔸_K → 𝔸_L
997. NumberField.AdeleRing.baseChangeAdeleEquiv The canonical 𝔸_K-algebra homeomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the base change map 𝔸_K → 𝔸_L
998. NumberField.AdeleRing.baseChangeEquiv' The canonical L-algebra isomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the K-algebra base change map 𝔸_K → 𝔸_L
999. NumberField.InfinitePlace.Completion.comapHom The map from v.Completion to w.Completion whenever the infinite place w of L lies above the infinite place v of K
1000. NumberField.InfinitePlace.Completion.piExtension The map from v.Completion to the product of all completions of L lying above v
1001. NumberField.InfinitePlace.Completion.baseChange The L-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtension
1002. NumberField.InfinitePlace.Completion.baseChangeRight The v.Completion-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtension
1003. NumberField.InfinitePlace.Completion.baseChangeEquiv The L-algebra homeomorphism between L ⊗[K] v.Completion and the product of all completions of L lying above v
1004. NumberField.InfinitePlace.Completion.piEquiv The Kᵥ-linear homeomorphism between Kᵥ^d and the product of all completions of L lying above v, where d = [K : L]
1005. strictMonoOn_Ici_nat_of_lt_succ upstream
1006. strictMonoOn_Ioi_nat_of_lt_succ upstream
1007. rootDiscrBound Minkowski's lower bound for the root discriminant (that is, the nth root of the absolute value of the discriminant) of a totally complex number field of degree n
1008. NumberField.InfiniteAdeleRing.baseChange The canonical map from the infinite adeles of K to the infinite adeles of L
1009. NumberField.InfiniteAdeleRing.piEquiv The $K_{\infty}$-linear homeomorphism $K_{\infty}^{[L:K]} \cong L_{\infty}$
1010. NumberField.InfiniteAdeleRing.baseChangeAlgEquiv The $L$-algebra isomorphism $L\otimes_K K_{\infty} \cong L_{\infty}$
1011. NumberField.ComplexEmbedding.IsExtension If L/K and f : K →+* ℂ, g : L →+* ℂ, then we say g is an extension of f if g restricted to K is f
1012. NumberField.ComplexEmbedding.IsMixedExtension If L/K and f : K →+* ℂ, g : L →+* ℂ, then g is a mixed extension of f if the image of f is real while the image of g is complex
1013. NumberField.ComplexEmbedding.IsUnmixedExtension If L/K and f : K →+* ℂ, g : L →+* ℂ, then g is an unmixed extension of f if g is an extension of f but is not a mixed extension
1014. NumberField.ComplexEmbedding.isExtensionEquivSum The extensions g : L →+* ℂ of f : K →+* ℂ are the direct sum of the mixed and the unmixed extensions
1015. NumberField.InfinitePlace.Extension Documented declaration: Extension
1016. NumberField.InfinitePlace.toExtension Any infinite place w of L is an extension of its restriction to K
1017. NumberField.InfinitePlace.Extension.IsLift If w is an infinite place of L lying above the infinite place v of K, then there are two possibilities: - w.embedding extends v.embedding
1018. NumberField.InfinitePlace.Extension.IsConjugateLift If w is an infinite place of L lying above the infinite place v of K, then there are two possibilities: - w.embedding extends v.embedding
1019. NumberField.InfinitePlace.RamifiedExtension For a given infinite place v of K, RamifiedExtension L v are all the infinite places of L / K that extend v and are ramified over K
1020. NumberField.InfinitePlace.UnramifiedExtension For a given infinite place v of K, UnramifiedExtension L v are all the infinite places of L / K that extend v and are unramified over K
1021. NumberField.InfinitePlace.Extension.toRamifiedExtension Construct a v.RamifiedExtension L term from a w : v.Extension L such that w.1.IsRamified K
1022. NumberField.InfinitePlace.Extension.toUnramifiedExtension Construct a v.UnramifiedExtension L term from a w : v.Extension L such that w.1.IsUnramified K
1023. RestrictedProduct.padicNatDen The smallest positive natural n : ℕ for which x p * n is a p-adic integer for all p
1024. RestrictedProduct.padicNum The element of (p : Nat.Primes) → ℤ_[p] obtained by multiplying by padicNatDen
1025. Algebra.UniformlyBoundedRank A family of local rings R i has uniformly bounded rank if for every k there exists a uniform bound on |R i / m(R i)^k| over all i
1026. PatchingAlgebra.Component The k-th component of the patching algebra: the ultraproduct of the rings R i / m(R i)^k along the ultrafilter F
1027. PatchingAlgebra.componentMap The transition ring homomorphism between components: Component j → Component k for k ≤ j, induced by R i / m^j → R i / m^k
1028. PatchingAlgebra.subring Documented declaration: subring
1029. PatchingAlgebra.subalgebra The patching algebra as a Λ-subalgebra of the product of components
1030. PatchingAlgebra The patching algebra: the inverse limit of the components R i / m^k glued along the ultrafilter F
1031. PatchingAlgebra.lift A continuous family of ring homomorphisms f i : R∞ →+* R i lifts uniquely to a ring homomorphism R∞ →+* PatchingAlgebra R F
1032. PatchingAlgebra.ofPi Auxiliary ring homomorphism from sequences ℕ → ∀ i, R i of representatives modulo the filter F to the product of components, used in the construction of incl
1033. PatchingAlgebra.incl The natural ring homomorphism from the product ∏ i, R i into PatchingAlgebra R F
1034. PatchingAlgebra.componentMapRingHom Functoriality on components: a family of local ring homomorphisms f i : R i →+* R' i induces a ring homomorphism between the k-th components of the two patching systems
1035. PatchingAlgebra.map Functoriality of PatchingAlgebra in the family of local rings
1036. PatchingAlgebra.mapEquiv A family of ring isomorphisms R i ≃+* R' i lifts to an isomorphism of patching algebras
1037. Module.UniformlyBoundedRank A family of R-modules M i has uniformly bounded rank if there exists a single bound n : ℕ such that for every i, the rank of M i over R / Ann (M i) is less than n
1038. PatchingModule.Component Documented declaration: Component
1039. PatchingModule.liftComponent A family of linear maps f i : M₀ →ₗ[R] M i lifts to a linear map M₀ / α • M₀ → Component α
1040. OpenIdeals The set of open ideals of a topological ring R
1041. PatchingModule.componentMap The transition linear map between components for ideals α ≤ β: Component α → Component β
1042. PatchingModule.submodule The patching module as a submodule of the product of components: those families compatible with the transition maps as α ≤ β ranges over open ideals
1043. PatchingModule The patching module for a family M i of modules over a commutative topological ring R
1044. PatchingModule.π The projection from the patching module onto its α-th component, for an open ideal α of R
1045. PatchingModule.ofPi Auxiliary linear map from indexed sequences of representatives to the product of components, used to construct PatchingModule.incl
1046. PatchingModule.incl The natural (ι → R)-linear map ∏ i, M i → PatchingModule R M F
1047. PatchingModule.componentMapModule Functoriality of PatchingModule.Component in the family of modules: a family of linear maps f i : M i →ₗ[R] N i induces a map between the α-th components
1048. PatchingModule.map Functoriality of PatchingModule in the family of modules
1049. PatchingModule.mapEquiv A family of linear equivalences M i ≃ₗ[R] N i lifts to a linear equivalence between the corresponding patching modules
1050. PatchingModule.toConst The natural map from a fixed module M to the patching module of the constant family fun _ ↦ M
1051. IsPatchingSystem A family of modules M i is a patching system along the filter F if for every open ideal α ⊆ R, the annihilator Ann (M i) is F-eventually contained in α
1052. Submodule.liftModIdeal Given a linear map f : M / I • M → N / I • N, produce the induced linear map between the corresponding quotients of M / J • M and N / J • N modulo I
1053. Submodule.liftModIdealEquiv Promote Submodule.liftModIdeal to a linear equivalence: a linear equivalence between R-modules M /IM and N/IN lifts to one between (M/JM)/I and (N/JM)/I
1054. PatchingModule.ker_componentMapModule_mkQ attribute [local instance] UltraProduct.instIsScalarTower in
1055. PatchingAlgebra.smulData Documented declaration: smulData
1056. eventuallyProd Given a filter F on the index set and a family of submodules N i ≤ M i, the submodule of Π i, M i consisting of those tuples v for which v i ∈ N i holds F-eventually
1057. UltraProduct The ultraproduct of a family of additive groups M i along a filter F: the quotient of Π i, M i by tuples that are zero F-eventually
1058. UltraProduct.π The canonical projection from the product Π i, R i to the ultraproduct as a ring homomorphism
1059. UltraProduct.πₗ The canonical projection from the product Π i, M i of R i-modules to the ultraproduct as a Π i, R i-linear map
1060. UltraProduct.instIsScalarTower making this an instance timesout everything
1061. UltraProduct.map A family of linear maps f i : M i →ₗ[R i] N i induces a linear map between the corresponding ultraproducts
1062. UltraProduct.mapRingHom A family of ring homomorphisms f i : R i →+* S i induces a ring homomorphism between the corresponding ultraproducts
1063. UltraProduct.exists_algEquiv_of_bddAbove_card Let R₀ be a topological ring, topologically of finite type (over ℤ)
1064. UltraProduct.exists_ringEquiv_of_bddAbove_card Let R₀ be a topological ring, topologically of finite type (over ℤ)
1065. UltraProduct.continuous_of_bddAbove_card Let R₀ be a topological ring, topologically of finite type (over ℤ)
1066. UltraProduct.surjective_of_bddAbove_card Let R₀ be a topological ring, topologically of finite type (over ℤ)
1067. IsLocalRing.IsAdicTopology Documented declaration: IsAdicTopology
1068. IsLocalRing.withIdeal The default WithIdeal structure on a local ring R, picking out the maximal ideal
1069. Group.subsingleton_of_pow_prime_eq_one A connected compact Hausdorff vector space over 𝔽_p is trivial
1070. Group.totallyDisconnected_of_pow_prime_eq_one A compact Hausdorff vector space over 𝔽_p is totally disconnected
1071. CommGroup.no_compact_automorphisms A connected compact Hausdorff abelian topological group does not admit a nontrivial compact group of automorphisms
1072. Module.depth Not sure if we should use IsRegular or IsWeaklyRegular
1073. Ideal.idealQuotientEquiv Bijection between ideals of R / I and ideals of R containing I, via comap/map along the quotient map
1074. Submodule.pi' The product of a family of submodules N i ≤ M i, viewed as a submodule of Π i, M i over the product ring Π i, R i
1075. LinearMap.piMap' A more dependent version of LinearMap.piMap, making a product of linear maps into a linear map over the product of rings
1076. TwoSidedIdeal.leAddSubgroup The largest two-sided ideal contained in a given additive subgroup G ≤ α: those x ∈ α whose two-sided span is contained in G
1077. ModuleTypeCardLT The type of all finite R-modules of cardinality less than N, presented as a sigma type over Fin N
1078. AlgebraTypeCardLT The type of all finite R-algebras of cardinality less than N, presented as a sigma type over Fin N
1079. TopologicalModuleTypeCardLT The type of all finite Hausdorff topological R-modules of cardinality less than N, with continuous scalar multiplication
1080. TopologicalAlgebraTypeCardLT The type of all finite Hausdorff topological R-algebras of cardinality less than N, with continuous scalar multiplication
1081. Algebra.TopologicallyFG An R-algebra S is topologically finitely generated if there is a finite subset s ⊆ S such that the R-subalgebra generated by s is dense in S
1082. vanishingFilter Documented declaration: vanishingFilter
1083. vanishingUltrafilter The vanishing ultrafilter of a prime ideal p of the product ring
1084. vanishingFilterGI The Galois insertion between filters on ι and ideals of Π i, R i (for nontrivial R i) formed by vanishingFilter and eventuallyProd ⊥
1085. FLT.Bosses.B1 B1 is the statement of FLT
1086. FLT.Bosses.B2 B2 is the statement that FLT is true for primes p ≥ 5
1087. FLT.Bosses.B3 B3 is the statement that there is no Frey Package
1088. FLT.Bosses.B4 B4 is the statement that if E is the Frey curve attached to a Frey package (a,b,c,p), then E[p] is a reducible Galois representation
1089. FLT.Bosses.B3_implies_B2 No Frey package implies FLT for primes at least 5 after FLT.Bosses.B2, FLT.Bosses.B3, FreyPackage.fermatLastTheoremFor_p_ge_5
1090. FLT.Bosses.B4_implies_B3 Reducible p-torsion rules out a Frey package after FLT.Bosses.B3, FLT.Bosses.B4, FreyPackage.mazur
1091. FLT.Bosses.B4_proof The remaining spine gap: the p-torsion is reducible (unproved) after FLT.Bosses.B4
1092. flt Fermat's Last Theorem, conditional on unfinished work after FLT.Bosses.B1, FLT.Bosses.B3_implies_B2, FLT.Bosses.B4_implies_B3, FLT.Bosses.B4_proof
1093. IsQuaternionAlgebra.NumberField.WithRigidification A rigidification of a quaternion algebra D over a number field F is a fixed choice of 𝔸_F^∞-algebra isomorphism D ⊗[F] 𝔸_F^∞ = M₂(𝔸_F^∞)
1094. IsQuaternionAlgebra.NumberField.WithRigidification.algEquiv Given a rigidification of D, D ⊗ 𝔸ᶠ is isomorphic to M₂(𝔸ᶠ)
1095. IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl Given a rigidification, we get an embedding Dˣ ↪ GL₂(𝔸_F)
1096. IsQuaternionAlgebra.NumberField.IsUnramified A quaternion algebra over a number field is unramified if it is split at all finite places
1097. IsDedekindDomain.M2.localFullLevel M_2(O_v) as a subring of M_2(F_v)
1098. IsDedekindDomain.GL2.localFullLevel GL₂(𝒪ᵥ) as a subgroup of GL₂(Fᵥ)
1099. IsDedekindDomain.GL2.localFullLevel.isOpen the clever way to prove this is a theorem of the form "if A is an open submonoid of R then Aˣ is an open subgroup of Rˣ"
1100. IsDedekindDomain.GL2.localFullLevel.isCompact the clever way to prove this is a theorem of the form "if A is a compact submonoid of R then Aˣ is a compact subgroup of Rˣ"
1101. IsDedekindDomain.GL2.localIwahoriLevel local U₀(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (* *;0 *) mod v
1102. IsDedekindDomain.GL2.localIwahoriLevel.isOpen the clever way to prove this is a theorem of the form "if A is an open submonoid of R then Aˣ is an open subgroup of Rˣ"
1103. IsDedekindDomain.GL2.localIwahoriLevel.isCompact the clever way to prove this is a theorem of the form "if A is a compact submonoid of R then Aˣ is a compact subgroup of Rˣ"
1104. IsDedekindDomain.GL2.localTameLevel local U_1(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (a *;0 a) mod v
1105. IsDedekindDomain.GL2.localTameLevel.isOpen the clever way to prove this is a theorem of the form "if A is an open submonoid of R then Aˣ is an open subgroup of Rˣ"
1106. IsDedekindDomain.GL2.localPTameLevel local U_1(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (a *;0 b) mod v with p ∤ ord_{k(v)}(a/b)
1107. IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion The canonical group homomorphism from GL_2(𝔸_F^∞) to the local component GL_2(F_v) for v a finite place
1108. IsDedekindDomain.FiniteAdeleRing._root_.RestrictedProduct.mulSingleHom RestrictedProduct.mulSingle as a MonoidHom
1109. IsDedekindDomain.FiniteAdeleRing.GL2.restrictedProduct GL_2(𝔸_F^∞) is isomorphic and homeomorphic to the restricted product of the local components GL_2(F_v)
1110. DimensionTheorem.colength The length of R ⧸ I as a natural number (junk value 0 when the length is infinite; see colength_coe for the case of an ideal of definition)
1111. DimensionTheorem.hilbertSamuel The Hilbert–Samuel function of a local ring: n ↦ ℓ(R ⧸ 𝔪ⁿ)
1112. DimensionTheorem.growthDeg The growth degree d(R) of the Hilbert–Samuel function: the least d such that ℓ(R ⧸ 𝔪ⁿ) = O(nᵈ)
1113. DimensionTheorem.minGenPrimary δ(R): the minimal number of generators of an ideal of definition of R, i.e. of an 𝔪-primary ideal (an ideal with radical 𝔪)
1114. DimensionTheorem.isArtinianRing_quotient_of_radical_eq A quotient by an ideal of definition is an Artinian ring
1115. DimensionTheorem.length_quotient_ne_top_of_radical_eq A quotient by an ideal of definition has finite length over R
1116. DimensionTheorem.colength_coe For an ideal of definition, colength really is the length
1117. DimensionTheorem.radical_pow_eq_of_radical_eq Powers of an ideal of definition are ideals of definition
1118. DimensionTheorem.colength_le_colength colength is antitone: a larger ideal has a smaller quotient
1119. DimensionTheorem.hilbertSamuel_monotone The Hilbert–Samuel function is monotone
1120. DimensionTheorem.length_quotient_eq_add Additivity of length along a pair of nested ideals I ≤ J, from the exact sequence 0 → J/I → R/I → R/J → 0 (valid in ℕ∞, no finiteness needed)
1121. DimensionTheorem.maximalIdeal_mem_minimalPrimes If I has radical 𝔪, then 𝔪 is minimal over I
1122. DimensionTheorem.ringKrullDim_le_minGenPrimary Dimension theorem, easy inequality: dim R ≤ δ(R), from Krull's height theorem
1123. DimensionTheorem.minGenPrimary_le_ringKrullDim Dimension theorem, converse inequality: δ(R) ≤ dim R; there exists a system of parameters, i.e. an 𝔪-primary ideal generated by dim R elements
1124. DimensionTheorem.ringKrullDim_eq_minGenPrimary dim R = δ(R) for a Noetherian local ring
1125. DimensionTheorem.map_mk_maximalIdeal The image of the maximal ideal in a proper quotient is the maximal ideal
1126. DimensionTheorem.length_quotient_map_quotient The length of a double quotient over R ⧸ I equals the length of the corresponding single quotient over R
1127. DimensionTheorem.hilbertSamuel_quotient_eq The Hilbert–Samuel function of R ⧸ I as a colength in R
1128. DimensionTheorem.hilbertSamuel_quotient_le The Hilbert–Samuel function decreases when passing to a proper quotient ring
1129. DimensionTheorem.exists_hilbertSamuel_quotient_span_singleton_add_le Artin–Rees difference bound
1130. DimensionTheorem.ringKrullDim_le_zero_of_growthLE_zero Base case: bounded Hilbert–Samuel function forces dimension ≤ 0
1131. DimensionTheorem.ringKrullDim_le_of_forall_minimalPrimes Reduction to domain quotients: to bound dim R it suffices to bound dim (R ⧸ p) for every minimal prime p
1132. DimensionTheorem.ringKrullDim_le_of_growthLE dim R ≤ d(R), inductive form: any bound on the growth of the Hilbert–Samuel function bounds the Krull dimension
1133. DimensionTheorem.multiset_prod_mem_pow A product of a multiset of elements of an ideal lies in the corresponding power of the ideal
1134. DimensionTheorem.monomial The degree-n monomial in the elements of s indexed by a symmetric power
1135. DimensionTheorem.span_pow_eq_span_monomial qⁿ is spanned by the degree-n monomials in a generating set of q
1136. DimensionTheorem.length_span_range_le A module spanned by finitely many elements each killed by q has length at most (number of generators) * length (R ⧸ q)
1137. DimensionTheorem.length_pow_quotient_le Documented declaration: length_pow_quotient_le
1138. DimensionTheorem.colength_pow_le Summing the filtration bounds: ℓ(R/qⁿ) is bounded by ℓ(R/q) * (n+1)^k where k = s.card ≥ 1
1139. DimensionTheorem.growthLE_hilbertSamuel_spanFinrank d(R) ≤ δ(R), main lemma: the Hilbert–Samuel function grows at most like n^k where k is the number of generators of any ideal of definition
1140. DimensionTheorem.growthLE_hilbertSamuel_growthDeg The defining set of growthDeg is nonempty; growthDeg is a true minimum
1141. DimensionTheorem.growthDeg_le_minGenPrimary d(R) ≤ δ(R)
1142. DimensionTheorem.ringKrullDim_le_growthDeg dim R ≤ d(R)
1143. DimensionTheorem.ringKrullDim_eq_growthDeg The dimension theorem for Noetherian local rings, first equality: the Krull dimension equals the growth degree of the Hilbert–Samuel function
1144. DimensionTheorem.dimension_theorem The dimension theorem for Noetherian local rings: dim R = d(R) = δ(R)
1145. DimensionTheorem.growthDeg_eq_minGenPrimary The three quantities as natural numbers: d(R) = δ(R)
1146. DimensionTheorem.GrowthLE f : ℕ → ℕ grows at most like n ^ d
1147. DimensionTheorem.GrowthLE.telescope_aux Telescoping lemma
1148. DimensionTheorem.GrowthLE.of_le_sub hc is kept for interface stability but is not actually needed: each application of h is at a point n + (j + 1) * c ≥ c regardless
1149. DimensionTheorem.multichoose_le_pow Documented declaration: multichoose_le_pow
1150. tsum_lambert_of_summable Documented declaration: tsum_lambert_of_summable
1151. isTopologicallyNilpotent_iff_tendsto_geomSum Documented declaration: isTopologicallyNilpotent_iff_tendsto_geomSum
1152. tsum_lambert_of_summable_of_isTopologicallyNilpotent Documented declaration: tsum_lambert_of_summable_of_isTopologicallyNilpotent
1153. hasSum_geometric_pow_mul_succ The geometric series of rᵐ, indexed from the first term: for ‖r‖ < 1 and m ≠ 0, ∑_{j≥1} r^{mj} = rᵐ/(1-rᵐ)
1154. summable_prod_mul_pow' The variant of summable_prod_mul_pow with the weight on the first coordinate
1155. Dickson.CyclicPartitionConfig Combinatorial data for one class in a cyclic partition: f conjugate cyclic subgroups, each of order d
1156. Dickson.HasCyclicPartition HasCyclicPartition G configs states that the finite group G is covered by cyclic subgroups (intersecting pairwise trivially) whose orders and conjugate counts match configs
1157. Dickson.FqInK The subfield 𝔽_{p^m} sitting inside K p = 𝔽̄_p, i.e. the set of x with x ^ (p ^ m) = x
1158. Dickson.translationGL The translation x ↦ x + b as the element !![1, b; 0, 1] of GL₂(K p)
1159. Dickson.dilationGL The dilation x ↦ c x (for c ≠ 0) as the element !![c, 0; 0, 1] of GL₂(K p)
1160. Dickson.translationPGL The translation x ↦ x + b as an element of PGLOf (K p) = PGL₂(𝔽̄_p)
1161. Dickson.dilationPGL The dilation x ↦ c x (for c ≠ 0) as an element of PGLOf (K p) = PGL₂(𝔽̄_p)
1162. Dickson.translationSet The set of b : K p for which the translation x ↦ x + b lies in the subgroup H
1163. Dickson.galoisFieldRingHom A ring embedding GaloisField p m →+* K p of 𝔽_{p^m} into 𝔽̄_p, with image FqInK p m
1164. Dickson.P1point The point [c : 1] of the projective line ℙ¹(𝔽̄_p) associated to c : K p
1165. Dickson.P1Fq The copy of ℙ¹(𝔽_q) (q = p^m) inside the projective line: ∞ together with the points [c : 1] for c ∈ 𝔽_{p^m}
1166. Dickson.orbitInfty The orbit of ∞ under the subgroup G', i.e. the set of points g • ∞ for g ∈ G'
1167. Dickson.dilationParam For g fixing ∞, the nonzero scalar c such that conjugation by g sends the translation by x to the translation by c x
1168. Dickson.normDilationParam The dilation parameter of an element g of the normalizer of the Sylow p-subgroup P, as a scalar in K p
1169. Dickson.conjEquiv The multiplicative isomorphism between G and its image k₀ G k₀⁻¹ under conjugation by k₀
1170. Dickson.sylowMap The image of the Sylow p-subgroup P under conjugation by k₀, as a Sylow p-subgroup of the conjugate group k₀ G k₀⁻¹
1171. Dickson.conjClassElements The finset of non-identity elements of G' lying in some conjugate of the subgroup H
1172. Dickson.conjNonidentity The finset of non-identity elements of the conjugate subgroup H.map (MulAut.conj g)
1173. Dickson.PGLOf The projective general linear group PGL₂(F) over a field F, i.e. GL₂(F) modulo its centre
1174. Dickson.ProjectiveLine The projective line ℙ¹(K p) over K p
1175. Dickson.glActionProjectiveLine The natural GL₂(K p)-action on the projective line ℙ¹(K p)
1176. Dickson.pglMap The group homomorphism PGL₂(F) → PGL₂(L) induced by a ring homomorphism f : F →+* L
1177. Dickson.fixedPoints The set of fixed points of the action of g : PGLOf (K p) on the projective line ℙ¹(K p)
1178. Dickson.infinity The point ∞ = [1 : 0] of the projective line ℙ¹(K p)
1179. SL2.E12 The elementary matrix e₁₂ a = !![1, a; 0, 1] as an element of SL₂(F)
1180. SL2.E21 The elementary matrix e₂₁ b = !![1, 0; b, 1] as an element of SL₂(F)
1181. SL2ToPGL The natural homomorphism SL₂(F) → PGL₂(F) sending a matrix to the class of its image in GL₂(F)
1182. PSLImageInPGL The image of PSL₂(F) inside PGL₂(F), namely the range of SL2ToPGL F
1183. SL2F3 The special linear group SL₂(𝔽₃)
1184. PSL2F3 The projective special linear group PSL₂(𝔽₃)
1185. p1Rep A choice of representative vector in 𝔽₃² for each of the four points of ℙ¹(𝔽₃)
1186. p1Proj Documented declaration: p1Proj
1187. p1Act The action of a matrix M on the four points of ℙ¹(𝔽₃), obtained by applying M to a representative vector and projecting back
1188. sl2F3ToPermHom The permutation representation SL₂(𝔽₃) → S₄ induced by the action on ℙ¹(𝔽₃)
1189. U₁ The upper elementary generator !![1, 1; 0, 1] of SL₂(𝔽₃)
1190. L₁ The lower elementary generator !![1, 0; 1, 1] of SL₂(𝔽₃)
1191. Dickson.sylowFixedPoint The unique fixed point on the projective line ℙ¹(𝔽̄_p) of a Sylow p-subgroup P
1192. Dickson.normalizerQuotient The index |N_G(P)| / |P| of a Sylow p-subgroup P in its normalizer in G
1193. Dickson.Phi The set of points on the projective line fixed by some non-identity element of G
1194. Dickson.PhiType The subtype of points on the projective line fixed by some non-identity element of G
1195. Dickson.instFintypeOfGroupOfFinite A finite group is a Fintype
1196. Dickson.pairStabilizer The subgroup of G consisting of the elements that fix both x and y on the projective line
1197. Dickson.dilationHomOfFix The group homomorphism from a finite subgroup H of PGLOf (K p) fixing infinity to (K p)ˣ, sending each element to its dilation parameter
1198. Dickson.partitionTerm A single summand 1 / sᵢ * (1 - 1 / zᵢ) appearing in the class-equation sum
1199. Slop.OddRepOrig.baseChange Compatibility alias for Slop.OddRep.baseChange
1200. Slop.OddRepOrig.adjoinRange Compatibility alias for Slop.OddRep.adjoinRange
1201. Slop.OddRepOrig.IsAbsolutelyIrreducible Compatibility alias for Slop.OddRep.IsAbsolutelyIrreducible
1202. Slop.OddRep.baseChange Base change of a representation along a field extension l/k: G acts on l ⊗[k] V by 1 ⊗ ρ(g)
1203. Slop.OddRep.adjoinRange The k-subalgebra A ⊆ End_k(V) generated by the image of ρ
1204. Slop.OddRep.IsAbsolutelyIrreducible A representation is absolutely irreducible if it remains irreducible after base change to an algebraic closure of k
1205. Slop.OddRep.smul_tmul_mem_range_iff Fact 1.1
1206. Slop.OddRep.exists_smul_eq_of_commute Lemma 1.4
1207. Slop.OddRep.adjoinRange_eq_top Lemma 1.5
1208. Slop.OddRep.adjoinRange_baseChange_eq_top Lemma 1.6
1209. Slop.OddRep.isIrreducible_of_adjoinRange_eq_top Documented declaration: isIrreducible_of_adjoinRange_eq_top
1210. Slop.OddRep.isIrreducible_of_baseChange Documented declaration: isIrreducible_of_baseChange
1211. Slop.OddRep.isIrreducible_baseChange_of_finrank_eigenspace_eq_one The quantitative version of the hard direction: under the hypotheses of Theorem 1.3, the base change of ρ to any field extension l/k is irreducible
1212. Slop.OddRep.isIrreducible_iff_isAbsolutelyIrreducible_slop Proposition 1.2 / Theorem 1.3
1213. PNat.pow_add_pow_ne_pow Fermat's Last Theorem for positive naturals