Loogle!

Result

Found 169 declarations mentioning IsAlgClosed.

• IsAlgClosed 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] : Prop
• IsAlgClosed.instInfinite 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {K : Type u_1} [Field K] [IsAlgClosed K] : Infinite K
• IsAlgClosed.perfectField 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] [IsAlgClosed k] : PerfectField k
• IsAlgClosed.mk 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] (splits : ∀ (p : Polynomial k), p.Splits) : IsAlgClosed k
• IsAlgClosed.splits 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} {inst✝ : Field k} [self : IsAlgClosed k] (p : Polynomial k) : p.Splits
• IsAlgClosed.exists_eq_mul_self 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] (x : k) : ∃ z, x = z * z
• IsAlgClosed.perfectRing 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] [IsAlgClosed k] : PerfectRing k p
• IsAlgClosed.card_roots_eq_natDegree 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots.card = p.natDegree
• IsAlgClosed.exists_pow_nat_eq 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z, z ^ n = x
• IsAlgClosed.eval_surjective 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {M : Type w} [Field M] [IsAlgClosed M] {p : Polynomial M} (hp : p.natDegree ≠ 0) : Function.Surjective fun x => Polynomial.eval x p
• IsAlgClosed.exists_root 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] (p : Polynomial k) (hp : p.degree ≠ 0) : ∃ x, p.IsRoot x
• IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots = 0 ↔ p.natDegree = 0
• IsAlgClosed.of_ringEquiv 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] (k' : Type u) [Field k'] (e : k ≃+* k') [IsAlgClosed k] : IsAlgClosed k'
• IsAlgClosure.isAlgClosed 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (R : Type u) {K : Type v} {inst✝ : CommRing R} {inst✝¹ : Field K} {inst✝² : Algebra R K} {inst✝³ : Module.IsTorsionFree R K} [self : IsAlgClosure R K] : IsAlgClosed K
• IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [Semiring A] [Field B] [IsAlgClosed B] (f : A →+* B) {p : Polynomial A} (h : IsUnit p.leadingCoeff) : (Polynomial.map f p).roots.card = p.natDegree
• IsAlgClosed.splits_domain 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u_1} {K : Type u_2} [Field k] [IsAlgClosed k] [Field K] {f : k →+* K} (p : Polynomial k) : (Polynomial.map f p).Splits
• IsAlgClosed.degree_eq_one_of_irreducible 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] [IsAlgClosed k] {p : Polynomial k} (hp : Irreducible p) : p.degree = 1
• IsAlgClosed.roots_eq_zero_iff_degree_nonpos 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots = 0 ↔ p.degree ≤ 0
• IsAlgClosure.mk 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {R : Type u} {K : Type v} [CommRing R] [Field K] [Algebra R K] [Module.IsTorsionFree R K] (isAlgClosed : IsAlgClosed K) (isAlgebraic : Algebra.IsAlgebraic R K) : IsAlgClosure R K
• IsAlgClosed.card_aroots_eq_natDegree 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [CommRing A] [Field B] [IsAlgClosed B] [Algebra A B] [FaithfulSMul A B] {p : Polynomial A} : (p.aroots B).card = p.natDegree
• IsAlgClosed.card_aroots_eq_natDegree_of_isUnit_leadingCoeff 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [CommRing A] [Field B] [IsAlgClosed B] [Algebra A B] {p : Polynomial A} (h : IsUnit p.leadingCoeff) : (p.aroots B).card = p.natDegree
• IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [Ring A] [IsSimpleRing A] [Field B] [IsAlgClosed B] (f : A →+* B) (p : Polynomial A) : (Polynomial.map f p).roots.card = p.natDegree
• IsAlgClosed.algebraMap_bijective_of_isIntegral 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u_1} {K : Type u_2} [Field k] [Ring K] [IsDomain K] [hk : IsAlgClosed k] [Algebra k K] [Algebra.IsIntegral k K] : Function.Bijective ⇑(algebraMap k K)
• IsAlgClosed.of_exists_root 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] (H : ∀ (p : Polynomial k), p.Monic → Irreducible p → ∃ x, Polynomial.eval x p = 0) : IsAlgClosed k
• IsAlgClosed.ringHom_bijective_of_isIntegral 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u_1} {K : Type u_2} [Field k] [CommRing K] [IsDomain K] [IsAlgClosed k] (f : k →+* K) (hf : f.IsIntegral) : Function.Bijective ⇑f
• IsAlgClosed.card_roots_map_eq_natDegree_of_injective 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [Semiring A] [Field B] [IsAlgClosed B] {f : A →+* B} (p : Polynomial A) (hf : Function.Injective ⇑f) : (Polynomial.map f p).roots.card = p.natDegree
• IsAlgClosed.exists_eval₂_eq_zero 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] {R : Type u_1} [Ring R] [IsSimpleRing R] [IsAlgClosed k] (f : R →+* k) (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ x, Polynomial.eval₂ f x p = 0
• IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [Semiring A] [Field B] [IsAlgClosed B] {f : A →+* B} {p : Polynomial A} (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).roots.card = p.natDegree
• IsAlgClosed.exists_eval₂_eq_zero_of_injective 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] {R : Type u_1} [Semiring R] [IsAlgClosed k] (f : R →+* k) (hf : Function.Injective ⇑f) (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ x, Polynomial.eval₂ f x p = 0
• IsAlgClosed.instIsAlgClosure 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (F : Type u_1) [Field F] [IsAlgClosed F] : IsAlgClosure F F
• IsAlgClosed.card_aroots_eq_natDegree_of_leadingCoeff_ne_zero 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {A : Type u_1} {B : Type u_2} [CommRing A] [Field B] [IsAlgClosed B] [Algebra A B] {p : Polynomial A} (hf : (algebraMap A B) p.leadingCoeff ≠ 0) : (p.aroots B).card = p.natDegree
• IsAlgClosed.lift 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {M : Type w} [Field M] [IsAlgClosed M] {R : Type u} [CommRing R] [IsDomain R] {S : Type v} [CommRing S] [IsDomain S] [Algebra R S] [Algebra R M] [Module.IsTorsionFree R S] [Module.IsTorsionFree R M] [Algebra.IsAlgebraic R S] : S →ₐ[R] M
• isAlgClosure_iff 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] (K : Type v) [Field K] [Algebra k K] : IsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K
• IsAlgClosed.nonempty_algEquiv_or_of_finrank_eq_two 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {F : Type u_1} {F' : Type u_2} (E : Type u_3) [Field F] [Field F'] [Field E] [Algebra F F'] [Algebra F E] [Algebra.IsAlgebraic F E] [IsAlgClosed F'] (h : Module.finrank F F' = 2) : Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
• IsAlgClosed.associated_iff_roots_eq_roots 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) : Associated p q ↔ p.roots = q.roots
• IsAlgClosed.exists_aeval_eq_zero 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] {R : Type u_1} [CommSemiring R] [IsAlgClosed k] [Algebra R k] [FaithfulSMul R k] (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ x, (Polynomial.aeval x) p = 0
• Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] [IsAlgClosed A] (x : K) : (Set.range fun ψ => ψ x) = (minpoly F x).rootSet A
• IsAlgClosed.roots_eq_zero_iff 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)
• IsAlgClosed.exists_aeval_eq_zero_of_injective 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] {R : Type u_1} [CommSemiring R] [IsAlgClosed k] [Algebra R k] (hinj : Function.Injective ⇑(algebraMap R k)) (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ x, (Polynomial.aeval x) p = 0
• IsAlgClosed.dvd_iff_roots_le_roots 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u} [Field k] [IsAlgClosed k] {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) : p ∣ q ↔ p.roots ≤ q.roots
• IsAlgClosed.surjective_domRestrict_of_isAlgebraic 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {K : Type u} [Field K] {L : Type v} {M : Type w} [Field L] [Algebra K L] [Field M] [Algebra K M] [IsAlgClosed M] {E : Type u_1} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsAlgebraic L E] : Function.Surjective fun φ => AlgHom.domRestrict L φ
• IsAlgClosed.surjective_restrictDomain_of_isAlgebraic 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {K : Type u} [Field K] {L : Type v} {M : Type w} [Field L] [Algebra K L] [Field M] [Algebra K M] [IsAlgClosed M] {E : Type u_1} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsAlgebraic L E] : Function.Surjective fun φ => AlgHom.domRestrict L φ
• IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {k : Type u_1} {K : Type u_2} [Field k] [Field K] [IsAlgClosed k] [Algebra k K] (L : IntermediateField k K) [Algebra.IsAlgebraic k ↥L] : L = ⊥
• Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  (k : Type u) [Field k] (K : Type v) [Field K] [IsAlgClosed K] [Algebra k K] (p q : Polynomial k) : IsCoprime p q ↔ ∀ (a : K), (Polynomial.aeval a) p ≠ 0 ∨ (Polynomial.aeval a) q ≠ 0
• Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] {f g : Polynomial K} (hf0 : f ≠ 0) : (∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ Polynomial.derivative f * g
• spectrum.nonempty_of_isAlgClosed_of_finiteDimensional 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  (𝕜 : Type u) {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] [Nontrivial A] [I : FiniteDimensional 𝕜 A] (a : A) : (spectrum 𝕜 a).Nonempty
• spectrum.map_pow_of_pos 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) : spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
• spectrum.map_pow_of_nonempty 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] {a : A} (ha : (spectrum 𝕜 a).Nonempty) (n : ℕ) : spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
• spectrum.map_polynomial_aeval_of_nonempty 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) (p : Polynomial 𝕜) (hnon : (spectrum 𝕜 a).Nonempty) : spectrum 𝕜 ((Polynomial.aeval a) p) = (fun k => Polynomial.eval k p) '' spectrum 𝕜 a
• spectrum.map_polynomial_aeval_of_degree_pos 📋 Mathlib.FieldTheory.IsAlgClosed.Spectrum
  {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) (p : Polynomial 𝕜) (hdeg : 0 < p.degree) : spectrum 𝕜 ((Polynomial.aeval a) p) = (fun x => Polynomial.eval x p) '' spectrum 𝕜 a
• Module.End.instInhabitedEigenvaluesOfIsAlgClosedOfFiniteDimensionalOfNontrivial 📋 Mathlib.LinearAlgebra.Eigenspace.Triangularizable
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : Module.End K V) : Inhabited f.Eigenvalues
• Module.End.exists_eigenvalue 📋 Mathlib.LinearAlgebra.Eigenspace.Triangularizable
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : Module.End K V) : ∃ c, f.HasEigenvalue c
• Module.End.iSup_maxGenEigenspace_eq_top 📋 Mathlib.LinearAlgebra.Eigenspace.Triangularizable
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] (f : Module.End K V) : ⨆ μ, f.maxGenEigenspace μ = ⊤
• LieModule.instIsTriangularizableOfIsAlgClosed 📋 Mathlib.Algebra.Lie.Weights.Basic
  (K : Type u_1) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] [IsAlgClosed K] : LieModule.IsTriangularizable K L M
• AlgebraicClosure.isAlgClosed 📋 Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
  (k : Type u) [Field k] : IsAlgClosed (AlgebraicClosure k)
• Module.End.IsSemisimple.eq_zero_iff_forall_eigenvalue 📋 Mathlib.LinearAlgebra.Eigenspace.Semisimple
  {K : Type u_3} {V : Type u_4} [Field K] [IsAlgClosed K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} (hf : f.IsSemisimple) : f = 0 ↔ ∀ (μ : K), f.HasEigenvalue μ → μ = 0
• Module.End.IsSemisimple.iSup_eigenspace_eq_top 📋 Mathlib.LinearAlgebra.Eigenspace.Semisimple
  {K : Type u_3} {V : Type u_4} [Field K] [IsAlgClosed K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} (hf : f.IsSemisimple) : ⨆ μ, f.eigenspace μ = ⊤
• AlgHom.card 📋 Mathlib.FieldTheory.PrimitiveElement
  (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] (K : Type u_3) [Field K] [IsAlgClosed K] [Algebra F K] : Fintype.card (E →ₐ[F] K) = Module.finrank F E
• Polynomial.natSepDegree_eq_of_isAlgClosed 📋 Mathlib.FieldTheory.SeparableDegree
  {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (f : Polynomial F) [DecidableEq E] [IsAlgClosed E] : f.natSepDegree = (f.aroots E).toFinset.card
• Field.embEquivOfIsAlgClosed 📋 Mathlib.FieldTheory.SeparableDegree
  (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra.IsAlgebraic F E] [IsAlgClosed K] : Field.Emb F E ≃ (E →ₐ[F] K)
• Field.finSepDegree_eq_of_isAlgClosed 📋 Mathlib.FieldTheory.SeparableDegree
  (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra.IsAlgebraic F E] [IsAlgClosed K] : Field.finSepDegree F E = Nat.card (E →ₐ[F] K)
• IsAlgClosed.algebraicClosure_eq_bot_iff 📋 Mathlib.FieldTheory.AlgebraicClosure
  (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [IsAlgClosed E] : algebraicClosure F E = ⊥ ↔ IsAlgClosed F
• algebraicClosure.isAlgClosure 📋 Mathlib.FieldTheory.AlgebraicClosure
  (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [IsAlgClosed E] : IsAlgClosure F ↥(algebraicClosure F E)
• IsSepClosed.of_isAlgClosed 📋 Mathlib.FieldTheory.IsSepClosed
  (k : Type u) [Field k] [IsAlgClosed k] : IsSepClosed k
• IsSepClosed.isAlgClosed_of_perfectField 📋 Mathlib.FieldTheory.IsSepClosed
  (k : Type u) [Field k] [IsSepClosed k] [PerfectField k] : IsAlgClosed k
• IsPurelyInseparable.of_injective_comp_algebraMap 📋 Mathlib.FieldTheory.PurelyInseparable.Basic
  (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : Type w) [Field L] [IsAlgClosed L] [Nonempty (E →+* L)] (h : Function.Injective fun f => f.comp (algebraMap F E)) : IsPurelyInseparable F E
• Algebra.FormallyUnramified.isField_of_isAlgClosed_of_isLocalRing 📋 Mathlib.RingTheory.Unramified.Field
  (K : Type u_1) (A : Type u_2) [Field K] [CommRing A] [Algebra K A] [Algebra.FormallyUnramified K A] [Algebra.EssFiniteType K A] [IsAlgClosed K] [IsLocalRing A] : IsField A
• Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_isLocalRing 📋 Mathlib.RingTheory.Unramified.Field
  (K : Type u_1) (A : Type u_2) [Field K] [CommRing A] [Algebra K A] [Algebra.FormallyUnramified K A] [Algebra.EssFiniteType K A] [IsAlgClosed K] [IsLocalRing A] : Function.Bijective ⇑(algebraMap K A)
• AlgebraicGeometry.residueFieldIsoBase 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) : X.residueField x ≅ CommRingCat.of K
• AlgebraicGeometry.pointOfClosedPoint 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X
• AlgebraicGeometry.pointEquivClosedPoint 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] : { p // CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K)) } ≃ ↑(closedPoints ↥X)
• AlgebraicGeometry.pointOfClosedPoint_comp 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pointOfClosedPoint f x hx) f = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))
• AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) : AlgebraicGeometry.Spec.map (AlgebraicGeometry.residueFieldIsoBase f x hx).inv = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f
• AlgebraicGeometry.pointOfClosedPoint_comp_assoc 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pointOfClosedPoint f x hx) (CategoryTheory.CategoryStruct.comp f h) = h
• AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv_assoc 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.residueFieldIsoBase f x hx).inv) h = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) (CategoryTheory.CategoryStruct.comp f h)
• AlgebraicGeometry.pointOfClosedPoint_apply 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) (a : ↥(AlgebraicGeometry.Spec (CommRingCat.of K))) : (AlgebraicGeometry.pointOfClosedPoint f x hx) a = x
• AlgebraicGeometry.ext_of_apply_closedPoint_eq 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] {f g : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X} (h : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType h] (hf : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))) (hg : CategoryTheory.CategoryStruct.comp g h = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K))) (H : f (IsLocalRing.closedPoint K) = g (IsLocalRing.closedPoint K)) : f = g
• AlgebraicGeometry.ext_of_apply_eq 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X Y : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] {f g : X ⟶ Y} (i : Y ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.IsSeparated i] [AlgebraicGeometry.LocallyOfFiniteType i] [AlgebraicGeometry.IsReduced X] [AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f i)] (S : Set ↥X) (hS : IsLocallyClosed S) (hS' : Dense S) (H : ∀ x ∈ S, IsClosed {x} → f x = g x) (H' : CategoryTheory.CategoryStruct.comp f i = CategoryTheory.CategoryStruct.comp g i) : f = g
• AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] (x : ↑(closedPoints ↥X)) : ↑((AlgebraicGeometry.pointEquivClosedPoint f).symm x) = AlgebraicGeometry.pointOfClosedPoint f ↑x ⋯
• AlgebraicGeometry.pointEquivClosedPoint_apply_coe 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.LocallyOfFiniteType f] (p : { p // CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K)) }) : ↑((AlgebraicGeometry.pointEquivClosedPoint f) p) = ↑p (IsLocalRing.closedPoint K)
• sum_smul_minpolyDiv_eq_X_pow 📋 Mathlib.FieldTheory.Minpoly.MinpolyDiv
  {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] (E : Type u_1) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K L] [Algebra.IsSeparable K L] {x : L} (hxL : K[x] = ⊤) {r : ℕ} (hr : r < Module.finrank K L) : ∑ σ, Polynomial.map (↑σ) ((x ^ r / (Polynomial.aeval x) (Polynomial.derivative (minpoly K x))) • minpolyDiv K x) = Polynomial.X ^ r
• Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans 📋 Mathlib.RingTheory.Trace.Basic
  (K : Type u_3) {L : Type u_4} [Field K] [Field L] [Algebra K L] {κ : Type w} (E : Type z) [Field E] [Algebra K E] [Module.Finite K L] [Algebra.IsSeparable K L] [IsAlgClosed E] (b : κ → L) [Fintype κ] (e : κ ≃ (L →ₐ[K] E)) : (Algebra.traceMatrix K b).map ⇑(algebraMap K E) = Algebra.embeddingsMatrixReindex K E b e * (Algebra.embeddingsMatrixReindex K E b e).transpose
• Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans 📋 Mathlib.RingTheory.Trace.Basic
  (K : Type u_3) {L : Type u_4} [Field K] [Field L] [Algebra K L] {κ : Type w} (E : Type z) [Field E] [Algebra K E] [Module.Finite K L] [Algebra.IsSeparable K L] [IsAlgClosed E] (b : κ → L) : (Algebra.traceMatrix K b).map ⇑(algebraMap K E) = Algebra.embeddingsMatrix K E b * (Algebra.embeddingsMatrix K E b).transpose
• trace_eq_sum_embeddings 📋 Mathlib.RingTheory.Trace.Basic
  {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E : Type u_6) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K L] [Algebra.IsSeparable K L] {x : L} : (algebraMap K E) ((Algebra.trace K L) x) = ∑ σ, σ x
• sum_embeddings_eq_finrank_mul 📋 Mathlib.RingTheory.Trace.Basic
  {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (F : Type u_5) [Field F] [Algebra L F] [Algebra K F] [IsScalarTower K L F] (E : Type u_6) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K F] [Algebra.IsSeparable K F] (pb : PowerBasis K L) : ∑ σ, σ ((algebraMap L F) pb.gen) = Module.finrank L F • ∑ σ, σ pb.gen
• Complex.isAlgClosed 📋 Mathlib.Analysis.Complex.Polynomial.Basic
  : IsAlgClosed ℂ
• NumberField.Embeddings.instNonemptyRingHom 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
  (K : Type u_1) [Field K] (A : Type u_2) [Field A] [CharZero A] [NumberField K] [IsAlgClosed A] : Nonempty (K →+* A)
• NumberField.Embeddings.instNonemptyRingHomOfIsAlgebraicRatOfIsAlgClosed 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
  (K : Type u_1) [Field K] (A : Type u_2) [Field A] [CharZero A] [CharZero K] [Algebra.IsAlgebraic ℚ K] [IsAlgClosed A] : Nonempty (K →+* A)
• NumberField.Embeddings.card 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
  (K : Type u_1) [Field K] (A : Type u_2) [Field A] [CharZero A] [NumberField K] [IsAlgClosed A] : Fintype.card (K →+* A) = Module.finrank ℚ K
• NumberField.Embeddings.finite_of_norm_le 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
  (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] (B : ℝ) : {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}.Finite
• NumberField.Embeddings.range_eval_eq_rootSet_minpoly 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
  (K : Type u_1) (A : Type u_2) [Field K] [NumberField K] [Field A] [Algebra ℚ A] [IsAlgClosed A] (x : K) : (Set.range fun φ => φ x) = (minpoly ℚ x).rootSet A
• NumberField.Embeddings.pow_eq_one_of_norm_eq_one 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
  (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {x : K} (hxi : IsIntegral ℤ x) (hx : ∀ (φ : K →+* A), ‖φ x‖ = 1) : ∃ n, ∃ (_ : 0 < n), x ^ n = 1
• NumberField.Embeddings.pow_eq_one_of_norm_le_one 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
  (K : Type u_1) [Field K] [NumberField K] (A : Type u_2) [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x) (hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1) : ∃ n, ∃ (_ : 0 < n), x ^ n = 1
• NumberField.Embeddings.coeff_bdd_of_norm_le 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
  {K : Type u_1} [Field K] [NumberField K] {A : Type u_2} [NormedField A] [IsAlgClosed A] [NormedAlgebra ℚ A] {B : ℝ} {x : K} (h : ∀ (φ : K →+* A), ‖φ x‖ ≤ B) (i : ℕ) : ‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ Module.finrank ℚ K * ↑((Module.finrank ℚ K).choose (Module.finrank ℚ K / 2))
• Algebra.prod_embeddings_eq_finrank_pow 📋 Mathlib.RingTheory.Norm.Basic
  {K : Type u_4} {L : Type u_5} (F : Type u_6) [Field K] [Field L] [Field F] [Algebra K L] [Algebra K F] (E : Type u_7) [Field E] [Algebra K E] [Algebra L F] [IsScalarTower K L F] [IsAlgClosed E] [Algebra.IsSeparable K F] [FiniteDimensional K F] (pb : PowerBasis K L) : ∏ σ, σ ((algebraMap L F) pb.gen) = (∏ σ, σ pb.gen) ^ Module.finrank L F
• AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed 📋 Mathlib.AlgebraicGeometry.Group.Abelian
  {K : Type u} [Field K] [IsAlgClosed K] (G : CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of K))) [AlgebraicGeometry.IsProper G.hom] [AlgebraicGeometry.IsIntegral (CategoryTheory.MonoidalCategoryStruct.tensorObj G G).left] [CategoryTheory.GrpObj G] : CategoryTheory.IsCommMonObj G
• Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosed 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
  {n : Type u_1} [Fintype n] [DecidableEq n] {F : Type u_3} [Field F] [IsAlgClosed F] : Matrix.ProjGenLinGroup n F ≃* Matrix.ProjectiveSpecialLinearGroup n F
• Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosedOfNonempty 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
  {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {F : Type u_3} [Field F] [IsAlgClosed F] : Matrix.ProjGenLinGroup n F ≃* Matrix.ProjectiveSpecialLinearGroup n F
• Algebra.norm_eq_prod_embeddings 📋 Mathlib.RingTheory.Norm.Transitivity
  {L : Type u_6} (K : Type u_7) [Field K] [Field L] [Algebra K L] (E : Type u_9) [Field E] [Algebra K E] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsAlgClosed E] (x : L) : (algebraMap K E) ((Algebra.norm K) x) = ∏ σ, σ x
• Matrix.det_eq_prod_roots_charpoly 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
  {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_3} [Field K] (A : Matrix n n K) [IsAlgClosed K] : A.det = A.charpoly.roots.prod
• Matrix.trace_eq_sum_roots_charpoly 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
  {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_3} [Field K] (A : Matrix n n K) [IsAlgClosed K] : A.trace = A.charpoly.roots.sum
• Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_one_mul_isMonicOfDegree 📋 Mathlib.Analysis.Polynomial.Factorization
  {F : Type u_1} [Field F] [IsAlgClosed F] {f : Polynomial F} {n : ℕ} (hf : f.IsMonicOfDegree (n + 1)) : ∃ f₁ f₂, f₁.IsMonicOfDegree 1 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
• IsAlgClosed.of_denseRange 📋 Mathlib.Analysis.Normed.Field.Dense
  {K : Type u_1} {L : Type u_2} [Field K] [NontriviallyNormedField L] [CompleteSpace L] [CharZero L] [IsUltrametricDist L] [Algebra K L] (hi : DenseRange ⇑(algebraMap K L)) [IsAlgClosed K] : IsAlgClosed L
• CategoryTheory.fieldEndOfFiniteDimensional 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X] [I : FiniteDimensional 𝕜 (X ⟶ X)] : Field (CategoryTheory.End X)
• CategoryTheory.finrank_endomorphism_simple_eq_one 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X : C) [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] : Module.finrank 𝕜 (X ⟶ X) = 1
• CategoryTheory.finrank_hom_simple_simple_le_one 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : Module.finrank 𝕜 (X ⟶ Y) ≤ 1
• CategoryTheory.finrank_hom_simple_simple 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C) [∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : Module.finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0
• CategoryTheory.finrank_endomorphism_eq_one 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] {X : C} (isIso_iff_nonzero : ∀ (f : X ⟶ X), CategoryTheory.IsIso f ↔ f ≠ 0) [I : FiniteDimensional 𝕜 (X ⟶ X)] : Module.finrank 𝕜 (X ⟶ X) = 1
• CategoryTheory.finrank_hom_simple_simple_eq_one_iff 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : Module.finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)
• CategoryTheory.finrank_hom_simple_simple_eq_zero_iff 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y] : Module.finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)
• CategoryTheory.endomorphism_simple_eq_smul_id 📋 Mathlib.CategoryTheory.Preadditive.Schur
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (𝕜 : Type u_2) [Field 𝕜] [IsAlgClosed 𝕜] [CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] {X : C} [CategoryTheory.Simple X] [FiniteDimensional 𝕜 (X ⟶ X)] (f : X ⟶ X) : ∃ c, c • CategoryTheory.CategoryStruct.id X = f
• IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt' 📋 Mathlib.FieldTheory.IsAlgClosed.Classification
  {R : Type u} [CommRing R] {K' : Type u} [Field K'] [Algebra R K'] [IsAlgClosed K'] {ι' : Type u} (v' : ι' → K') [Nontrivial R] (hv : IsTranscendenceBasis R v') (hR : Cardinal.mk R ≤ Cardinal.aleph0) (hK : Cardinal.aleph0 < Cardinal.mk K') : Cardinal.mk K' = Cardinal.mk ι'
• IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt 📋 Mathlib.FieldTheory.IsAlgClosed.Classification
  {R : Type u} {K : Type v} [CommRing R] [Field K] [Algebra R K] [IsAlgClosed K] {ι : Type w} (v : ι → K) [Nontrivial R] (hv : IsTranscendenceBasis R v) (hR : Cardinal.mk R ≤ Cardinal.aleph0) (hK : Cardinal.aleph0 < Cardinal.mk K) : Cardinal.lift.{w, v} (Cardinal.mk K) = Cardinal.lift.{v, w} (Cardinal.mk ι)
• IsAlgClosed.cardinal_le_max_transcendence_basis' 📋 Mathlib.FieldTheory.IsAlgClosed.Classification
  {R : Type u} [CommRing R] {K' : Type u} [Field K'] [Algebra R K'] [IsAlgClosed K'] {ι' : Type u} (v' : ι' → K') (hv : IsTranscendenceBasis R v') : Cardinal.mk K' ≤ max (max (Cardinal.mk R) (Cardinal.mk ι')) Cardinal.aleph0
• IsAlgClosed.cardinal_le_max_transcendence_basis 📋 Mathlib.FieldTheory.IsAlgClosed.Classification
  {R : Type u} {K : Type v} [CommRing R] [Field K] [Algebra R K] [IsAlgClosed K] {ι : Type w} (v : ι → K) (hv : IsTranscendenceBasis R v) : Cardinal.lift.{max u w, v} (Cardinal.mk K) ≤ max (max (Cardinal.lift.{max v w, u} (Cardinal.mk R)) (Cardinal.lift.{max u v, w} (Cardinal.mk ι))) Cardinal.aleph0
• IsAlgClosed.ringEquiv_of_equiv_of_charZero 📋 Mathlib.FieldTheory.IsAlgClosed.Classification
  {K : Type u} {L : Type v} [Field K] [Field L] [IsAlgClosed K] [IsAlgClosed L] [CharZero K] [CharZero L] (hK : Cardinal.aleph0 < Cardinal.mk K) (hKL : Nonempty (K ≃ L)) : Nonempty (K ≃+* L)
• IsAlgClosed.ringEquiv_of_equiv_of_char_eq 📋 Mathlib.FieldTheory.IsAlgClosed.Classification
  {K : Type u} {L : Type v} [Field K] [Field L] [IsAlgClosed K] [IsAlgClosed L] (p : ℕ) [CharP K p] [CharP L p] (hK : Cardinal.aleph0 < Cardinal.mk K) (hKL : Nonempty (K ≃ L)) : Nonempty (K ≃+* L)
• IsAlgClosed.equivOfTranscendenceBasis 📋 Mathlib.FieldTheory.IsAlgClosed.Classification
  {R : Type u_1} {L : Type u_2} {K : Type u_3} [CommRing R] [Field K] [Algebra R K] [Field L] [Algebra R L] {ι : Type u_4} (v : ι → K) {κ : Type u_5} (w : κ → L) [IsAlgClosed K] [IsAlgClosed L] (e : ι ≃ κ) (hv : IsTranscendenceBasis R v) (hw : IsTranscendenceBasis R w) : K ≃+* L
• IsAlgClosed.isAlgClosure_of_transcendence_basis 📋 Mathlib.FieldTheory.IsAlgClosed.Classification
  {R : Type u_1} {K : Type u_3} [CommRing R] [Field K] [Algebra R K] {ι : Type u_4} (v : ι → K) [IsAlgClosed K] (hv : IsTranscendenceBasis R v) : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K
• FirstOrder.Field.isAlgClosed_of_model_ACF 📋 Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
  (p : ℕ) (K : Type u_2) [Field K] [FirstOrder.Ring.CompatibleRing K] [h : K ⊨ FirstOrder.Language.Theory.ACF p] : IsAlgClosed K
• FirstOrder.Field.instModelACFOfCharPOfIsAlgClosed 📋 Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
  {K : Type u_1} [Field K] [FirstOrder.Ring.CompatibleRing K] {p : ℕ} [CharP K p] [IsAlgClosed K] : K ⊨ FirstOrder.Language.Theory.ACF p
• MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton 📋 Mathlib.RingTheory.Nullstellensatz
  {K : Type u_2} [Field K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] {I : Ideal (MvPolynomial σ K)} : I.IsMaximal ↔ ∃ x, I = MvPolynomial.vanishingIdeal K {x}
• MvPolynomial.vanishingIdeal_zeroLocus_eq_radical 📋 Mathlib.RingTheory.Nullstellensatz
  {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] (I : Ideal (MvPolynomial σ k)) : MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus K I) = I.radical
• MvPolynomial.IsPrime.vanishingIdeal_zeroLocus 📋 Mathlib.RingTheory.Nullstellensatz
  {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] (P : Ideal (MvPolynomial σ k)) [h : P.IsPrime] : MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus K P) = P
• MvPolynomial.eq_vanishingIdeal_singleton_of_isMaximal 📋 Mathlib.RingTheory.Nullstellensatz
  {k : Type u_1} (K : Type u_2) [Field k] [Field K] [Algebra k K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] {I : Ideal (MvPolynomial σ k)} (hI : I.IsMaximal) : ∃ x, I = MvPolynomial.vanishingIdeal k {x}
• ax_grothendieck_univ 📋 Mathlib.FieldTheory.AxGrothendieck
  {K : Type u_1} {ι : Type u_2} [Field K] [IsAlgClosed K] [Finite ι] (p : ι → MvPolynomial ι K) : (Function.Injective fun v i => (MvPolynomial.eval v) (p i)) → Function.Surjective fun v i => (MvPolynomial.eval v) (p i)
• ax_grothendieck_zeroLocus 📋 Mathlib.FieldTheory.AxGrothendieck
  {K : Type u_1} {ι : Type u_2} [Field K] [IsAlgClosed K] [Finite ι] (I : Ideal (MvPolynomial ι K)) (p : ι → MvPolynomial ι K) : have S := MvPolynomial.zeroLocus K I; Set.MapsTo (fun v i => (MvPolynomial.eval v) (p i)) S S → Set.InjOn (fun v i => (MvPolynomial.eval v) (p i)) S → Set.SurjOn (fun v i => (MvPolynomial.eval v) (p i)) S S
• ax_grothendieck_of_definable 📋 Mathlib.FieldTheory.AxGrothendieck
  {K : Type u_1} {ι : Type u_2} [Field K] [IsAlgClosed K] [Finite ι] [FirstOrder.Ring.CompatibleRing K] {c : Set K} (S : Set (ι → K)) (hS : c.Definable FirstOrder.Language.ring S) (ps : ι → MvPolynomial ι K) : Set.MapsTo (fun v i => (MvPolynomial.eval v) (ps i)) S S → Set.InjOn (fun v i => (MvPolynomial.eval v) (ps i)) S → Set.SurjOn (fun v i => (MvPolynomial.eval v) (ps i)) S S
• QuadraticForm.isometryEquivSumSquares 📋 Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
  {ι : Type u_1} [Fintype ι] {K : Type u_2} [Field K] [IsAlgClosed K] [DecidableEq K] (w : ι → K) : (QuadraticMap.weightedSumSquares K w).IsometryEquiv (QuadraticMap.weightedSumSquares K fun i => if w i = 0 then 0 else 1)
• QuadraticForm.isometryEquivSumSquaresUnits 📋 Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
  {ι : Type u_1} [Fintype ι] {K : Type u_2} [Field K] [IsAlgClosed K] [DecidableEq K] (w : ι → Kˣ) : (QuadraticMap.weightedSumSquares K w).IsometryEquiv (QuadraticMap.weightedSumSquares K 1)
• QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed 📋 Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
  {K : Type u_2} [Field K] [IsAlgClosed K] [Invertible 2] {M : Type u_3} [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) (hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)) : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K 1)
• QuadraticForm.equivalent_of_isAlgClosed 📋 Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
  {K : Type u_2} [Field K] [IsAlgClosed K] [Invertible 2] {M : Type u_3} [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q₁ Q₂ : QuadraticForm K M) (hQ₁ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₁)) (hQ₂ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₂)) : QuadraticMap.Equivalent Q₁ Q₂
• RootPairing.GeckConstruction.instHasTrivialRadical 📋 Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
  {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [Field K] [CharZero K] [DecidableEq ι] [Fintype ι] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootPairing ι K M N} [P.IsRootSystem] [P.IsCrystallographic] {b : P.Base} [P.IsReduced] [P.IsIrreducible] [IsAlgClosed K] : LieAlgebra.HasTrivialRadical K ↥(RootPairing.GeckConstruction.lieAlgebra b)
• RootPairing.GeckConstruction.instIsSimpleSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebra 📋 Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
  {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootPairing ι K M N} [P.IsReduced] [P.IsCrystallographic] [P.IsIrreducible] [P.IsRootSystem] (b : P.Base) [IsAlgClosed K] : LieAlgebra.IsSimple K ↥(RootPairing.GeckConstruction.lieAlgebra b)
• RootPairing.GeckConstruction.equivRootSystem 📋 Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
  {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [DecidableEq ι] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootPairing ι K M N} [P.IsReduced] [P.IsCrystallographic] [P.IsIrreducible] [P.IsRootSystem] (b : P.Base) [IsAlgClosed K] : P.Equiv (LieAlgebra.IsKilling.rootSystem (RootPairing.GeckConstruction.cartanSubalgebra' b))
• RootPairing.GeckConstruction.equivLieAlgebra 📋 Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
  {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {L : Type u_2} [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsSimple K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : L ≃ₗ⁅K⁆ ↥(RootPairing.GeckConstruction.lieAlgebra b)
• Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two 📋 Mathlib.RingTheory.Discriminant
  {ι : Type w} [DecidableEq ι] [Fintype ι] (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (b : ι → L) [Algebra.IsSeparable K L] (e : ι ≃ (L →ₐ[K] E)) : (algebraMap K E) (Algebra.discr K b) = (Algebra.embeddingsMatrixReindex K E b e).det ^ 2
• Algebra.discr_powerBasis_eq_prod 📋 Mathlib.RingTheory.Discriminant
  (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) (e : Fin pb.dim ≃ (L →ₐ[K] E)) [Algebra.IsSeparable K L] : (algebraMap K E) (Algebra.discr K ⇑pb.basis) = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2
• Algebra.discr_powerBasis_eq_prod' 📋 Mathlib.RingTheory.Discriminant
  (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) [Algebra.IsSeparable K L] (e : Fin pb.dim ≃ (L →ₐ[K] E)) : (algebraMap K E) (Algebra.discr K ⇑pb.basis) = ∏ i, ∏ j > i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))
• Algebra.discr_powerBasis_eq_prod'' 📋 Mathlib.RingTheory.Discriminant
  (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) [Algebra.IsSeparable K L] (e : Fin pb.dim ≃ (L →ₐ[K] E)) : (algebraMap K E) (Algebra.discr K ⇑pb.basis) = (-1) ^ (Module.finrank K L * (Module.finrank K L - 1) / 2) * ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)
• PadicComplex.isAlgClosed 📋 Mathlib.NumberTheory.Padics.Complex
  (p : ℕ) [hp : Fact (Nat.Prime p)] : IsAlgClosed ℂ_[p]
• IsSimpleModule.finrank_eq_one_of_isMulCommutative 📋 Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
  (A : Type u_1) (V : Type u_2) (k : Type u_3) [Field k] [Ring A] [Algebra k A] [AddCommGroup V] [Module k V] [Module A V] [IsScalarTower k A V] [IsSimpleModule A V] [FiniteDimensional k V] [IsAlgClosed k] [IsMulCommutative A] : Module.finrank k V = 1
• IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed 📋 Mathlib.RepresentationTheory.AlgebraRepresentation.Basic
  {A : Type u_1} {V : Type u_2} (k : Type u_3) [Field k] [Ring A] [Algebra k A] [AddCommGroup V] [Module k V] [Module A V] [IsScalarTower k A V] [IsSimpleModule A V] [FiniteDimensional k V] [IsAlgClosed k] : Function.Bijective ⇑(algebraMap k (Module.End A V))
• FDRep.finrank_hom_simple_simple 📋 Mathlib.RepresentationTheory.FDRep
  {k : Type u} {G : Type v} [Field k] [Monoid G] [IsAlgClosed k] (V W : FDRep k G) [CategoryTheory.Simple V] [CategoryTheory.Simple W] : Module.finrank k (V ⟶ W) = if Nonempty (V ≅ W) then 1 else 0
• Representation.IsIrreducible.finrank_eq_one_of_isMulCommutative 📋 Mathlib.RepresentationTheory.Irreducible
  {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [ρ.IsIrreducible] [FiniteDimensional k V] [IsAlgClosed k] [IsMulCommutative G] : Module.finrank k V = 1
• Representation.IsIrreducible.finrank_intertwiningMap_self 📋 Mathlib.RepresentationTheory.Irreducible
  {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [ρ.IsIrreducible] [FiniteDimensional k V] [IsAlgClosed k] : Module.finrank k (ρ.IntertwiningMap ρ) = 1
• Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed 📋 Mathlib.RepresentationTheory.Irreducible
  {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] {ρ : Representation k G V} [ρ.IsIrreducible] [FiniteDimensional k V] [IsAlgClosed k] : Function.Bijective ⇑(algebraMap k (ρ.IntertwiningMap ρ))
• Representation.char_orthonormal 📋 Mathlib.RepresentationTheory.Character
  {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Group G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) [Fintype G] [Invertible ↑(Nat.card G)] [IsAlgClosed k] [ρ.IsIrreducible] [σ.IsIrreducible] : (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0
• FDRep.char_orthonormal 📋 Mathlib.RepresentationTheory.Character
  {k : Type u} [Field k] {G : Type v} [Group G] [IsAlgClosed k] [Fintype G] [Invertible ↑(Nat.card G)] (V W : FDRep k G) [CategoryTheory.Simple V] [CategoryTheory.Simple W] : (↑(Nat.card G))⁻¹ * ∑ g, V.character g * W.character g⁻¹ = if Nonempty (V ≅ W) then 1 else 0
• FDRep.simple_iff_char_is_norm_one 📋 Mathlib.RepresentationTheory.FinGroupCharZero
  {k : Type u} [Field k] {G : Type u} [Group G] [IsAlgClosed k] [CharZero k] [Fintype G] (V : FDRep k G) : CategoryTheory.Simple V ↔ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
• FDRep.simple_iff_end_is_rank_one 📋 Mathlib.RepresentationTheory.FinGroupCharZero
  {k : Type u} [Field k] {G : Type u} [Finite G] [Group G] [IsAlgClosed k] [NeZero ↑(Nat.card G)] (V : FDRep k G) : CategoryTheory.Simple V ↔ Module.finrank k (V ⟶ V) = 1
• IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed 📋 Mathlib.RingTheory.SimpleModule.IsAlgClosed
  (F : Type u_1) (R : Type u_2) [Field F] [IsAlgClosed F] [Ring R] [Algebra F R] [IsSimpleRing R] [FiniteDimensional F R] : ∃ n, ∃ (_ : NeZero n), Nonempty (R ≃ₐ[F] Matrix (Fin n) (Fin n) F)
• IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed 📋 Mathlib.RingTheory.SimpleModule.IsAlgClosed
  (F : Type u_1) (R : Type u_2) [Field F] [IsAlgClosed F] [Ring R] [Algebra F R] [IsSemisimpleRing R] [FiniteDimensional F R] : ∃ n d, (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[F] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) F)
• WittVector.RecursionBase.solution 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] (a₁ a₂ : WittVector p k) : k
• WittVector.frobeniusRotationCoeff 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : ℕ → k
• WittVector.frobeniusRotation 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : WittVector p k
• WittVector.RecursionBase.solution_pow 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] (a₁ a₂ : WittVector p k) : ∃ x, x ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
• WittVector.RecursionBase.solution_spec 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] (a₁ a₂ : WittVector p k) : WittVector.RecursionBase.solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
• WittVector.RecursionBase.solution_nonzero 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : WittVector.RecursionBase.solution p a₁ a₂ ≠ 0
• WittVector.RecursionMain.succNthVal 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : k
• WittVector.frobeniusRotation_nonzero 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : WittVector.frobeniusRotation p ha₁ ha₂ ≠ 0
• WittVector.RecursionMain.root_exists 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : ∃ b, (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot b
• WittVector.RecursionMain.succNthVal_spec 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot (WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂)
• WittVector.RecursionBase.solution_spec' 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [IsAlgClosed k] {a₁ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (a₂ : WittVector p k) : WittVector.RecursionBase.solution p a₁ a₂ ^ p * a₁.coeff 0 = WittVector.RecursionBase.solution p a₁ a₂ * a₂.coeff 0
• WittVector.frobenius_frobeniusRotation 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a₁ a₂ : WittVector p k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : WittVector.frobenius (WittVector.frobeniusRotation p ha₁ ha₂) * a₁ = WittVector.frobeniusRotation p ha₁ ha₂ * a₂
• WittVector.RecursionMain.succNthVal_spec' 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (n : ℕ) (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + WittVector.nthRemainder p n (fun v => bs v ^ p) (WittVector.truncateFun (n + 1) a₁) = WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) + WittVector.nthRemainder p n bs (WittVector.truncateFun (n + 1) a₂)
• WittVector.exists_frobenius_solution_fractionRing 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] {a : FractionRing (WittVector p k)} (ha : a ≠ 0) : ∃ b, b ≠ 0 ∧ ∃ m, (IsFractionRing.ringEquivOfRingEquiv (WittVector.frobeniusEquiv p k)) b * a = ↑p ^ m * b
• WittVector.exists_frobenius_solution_fractionRing_aux 📋 Mathlib.RingTheory.WittVector.FrobeniusFractionField
  (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [Field k] [CharP k p] [IsAlgClosed k] (m n : ℕ) (r' q' : WittVector p k) (hr' : r'.coeff 0 ≠ 0) (hq' : q'.coeff 0 ≠ 0) (hq : ↑p ^ n * q' ∈ nonZeroDivisors (WittVector p k)) : have b := WittVector.frobeniusRotation p hr' hq'; (IsFractionRing.ringEquivOfRingEquiv (WittVector.frobeniusEquiv p k)) ((algebraMap (WittVector p k) (FractionRing (WittVector p k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ = ↑p ^ (↑m - ↑n) * (algebraMap (WittVector p k) (FractionRing (WittVector p k))) b
• WittVector.isocrystal_classification 📋 Mathlib.RingTheory.WittVector.Isocrystal
  (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_2) [Field k] [IsAlgClosed k] [CharP k p] (V : Type u_3) [AddCommGroup V] [WittVector.Isocrystal p k V] (h_dim : Module.finrank (FractionRing (WittVector p k)) V = 1) : ∃ m, Nonempty (WittVector.IsocrystalEquiv p k (WittVector.StandardOneDimIsocrystal p k m) V)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c