ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>Ring R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<GOAL>(∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * g x.2 = f n
<VAR>R : Type u_1<VAR>CommGroup R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<GOAL>(∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n
<VAR>R : Type u_1<VAR>CommGroupWithZero R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>f g : ℕ → R<VAR>hf : ∀ n > 0, f n ≠ 0<VAR>hg : ∀ n > 0, g n ≠ 0<GOAL>(∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n.divisors.card = ∏ x ∈ n.primeFactors, (n.factorization x + 1)
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ Finset.range (n.factorization p + 1), p ^ k
<VAR>m n : ℕ<VAR>hmn : m.Coprime n<GOAL>(m * n).divisors.card = m.divisors.card * n.divisors.card
<VAR>m n : ℕ<VAR>hmn : m.Coprime n<GOAL>∑ d ∈ (m * n).divisors, d = (∑ d ∈ m.divisors, d) * ∑ d ∈ n.divisors, d
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>g : G<VAR>v : V<GOAL>((Representation.trivial k) g) v = v
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>self : ρ.IsTrivial<VAR>g : G<VAR>x : V<GOAL>(ρ g) x = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>g : G<VAR>x : V<VAR>h : ρ.IsTrivial<GOAL>(ρ g) x = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<GOAL>ρ.asAlgebraHom = (MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>g : G<VAR>r : k<GOAL>ρ.asAlgebraHom (Finsupp.single g r) = r • ρ g
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>g : G<GOAL>ρ.asAlgebraHom (Finsupp.single g 1) = ρ g
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>g : G<GOAL>ρ.asAlgebraHom ((MonoidAlgebra.of k G) g) = ρ g
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>r : MonoidAlgebra k G<VAR>x : ρ.asModule<GOAL>ρ.asModuleEquiv (r • x) = (ρ.asAlgebraHom r) (ρ.asModuleEquiv x)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>r : k<VAR>x : V<GOAL>ρ.asModuleEquiv.symm (r • x) = (algebraMap k (MonoidAlgebra k G)) r • ρ.asModuleEquiv.symm x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>g : G<VAR>x : V<GOAL>ρ.asModuleEquiv.symm ((ρ g) x) = (MonoidAlgebra.of k G) g • ρ.asModuleEquiv.symm x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>CommSemiring k<VAR>Monoid G<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Module (MonoidAlgebra k G) M<VAR>r : MonoidAlgebra k G<VAR>m : RestrictScalars k (MonoidAlgebra k G) M<GOAL>((Representation.ofModule M).asAlgebraHom r) m = (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>g : G<VAR>x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule<GOAL>((Representation.ofModule ρ.asModule) g) x = (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x))))
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>CommSemiring k<VAR>Monoid G<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Module (MonoidAlgebra k G) M<VAR>r : MonoidAlgebra k G<VAR>m : (Representation.ofModule M).asModule<GOAL>(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((Representation.ofModule M).asModuleEquiv (r • m)) = r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((Representation.ofModule M).asModuleEquiv m)
<VAR>k : Type u_1<VAR>CommSemiring k<VAR>G : Type u_2<VAR>Monoid G<VAR>H : Type u_3<VAR>MulAction G H<VAR>g : G<GOAL>(Representation.ofMulAction k G H) g = Finsupp.lmapDomain k k fun x => g • x
<VAR>k : Type u_1<VAR>CommSemiring k<VAR>G : Type u_2<VAR>Monoid G<VAR>H : Type u_3<VAR>MulAction G H<VAR>g : G<VAR>x : H<VAR>r : k<GOAL>((Representation.ofMulAction k G H) g) (Finsupp.single x r) = Finsupp.single (g • x) r
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid A<VAR>Module k A<VAR>DistribMulAction G A<VAR>SMulCommClass G k A<VAR>g : G<VAR>a : A<GOAL>((Representation.ofDistribMulAction k G A) g) a = g • a
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>Monoid M<VAR>CommGroup G<VAR>MulDistribMulAction M G<VAR>g : M<VAR>a : Additive G<GOAL>((Representation.ofMulDistribMulAction M G) g) a = Additive.ofMul (g • Additive.toMul a)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>CommSemiring k<VAR>Group G<VAR>H : Type u_4<VAR>MulAction G H<VAR>g : G<VAR>f : H →₀ k<VAR>h : H<GOAL>(((Representation.ofMulAction k G H) g) f) h = f (g⁻¹ • h)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>CommSemiring k<VAR>Group G<VAR>x : MonoidAlgebra k G<VAR>y : (Representation.ofMulAction k G G).asModule<GOAL>x • y = x * y
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>CommSemiring k<VAR>Group G<GOAL>∀ (a : G →₀ k), Representation.ofMulActionSelfAsModuleEquiv.symm a = (Representation.ofMulAction k G G).asModuleEquiv.invFun a
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>CommSemiring k<VAR>Group G<GOAL>∀ (a : (Representation.ofMulAction k G G).asModule), Representation.ofMulActionSelfAsModuleEquiv a = (Representation.ofMulAction k G G).asModuleEquiv.toFun a
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>g : G<GOAL>↑(ρ.asGroupHom g) = ρ g
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>AddCommMonoid W<VAR>Module k W<VAR>ρV : Representation k G V<VAR>ρW : Representation k G W<VAR>g : G<GOAL>(ρV.tprod ρW) g = TensorProduct.map (ρV g) (ρW g)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>AddCommMonoid W<VAR>Module k W<VAR>ρV : Representation k G V<VAR>r : MonoidAlgebra k G<VAR>x : V<VAR>y : W<GOAL>let x' := x;
r • z = (r • x') ⊗ₜ[k] y
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommSemiring k<VAR>Monoid G<VAR>AddCommMonoid V<VAR>Module k V<VAR>AddCommMonoid W<VAR>Module k W<VAR>ρW : Representation k G W<VAR>r : MonoidAlgebra k G<VAR>x : V<VAR>y : W<GOAL>let y' := y;
r • z = x ⊗ₜ[k] (r • y')
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>AddCommMonoid W<VAR>Module k W<VAR>ρV : Representation k G V<VAR>ρW : Representation k G W<VAR>g : G<VAR>f : V →ₗ[k] W<GOAL>((ρV.linHom ρW) g) f = ρW g ∘ₗ f ∘ₗ ρV g⁻¹
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρV : Representation k G V<VAR>g : G<GOAL>ρV.dual g = Module.Dual.transpose (ρV g⁻¹)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>AddCommMonoid W<VAR>Module k W<VAR>ρV : Representation k G V<VAR>ρW : Representation k G W<VAR>g : G<GOAL>dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) = (ρV.linHom ρW) g ∘ₗ dualTensorHom k V W
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>CommSemiring k<VAR>Group G<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<VAR>g : G<GOAL>Finsupp.single g 1 * GroupAlgebra.average k G = GroupAlgebra.average k G
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>CommSemiring k<VAR>Group G<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<VAR>g : G<GOAL>GroupAlgebra.average k G * Finsupp.single g 1 = GroupAlgebra.average k G
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>v : V<GOAL>v ∈ ρ.invariants ↔ ∀ (g : G), (ρ g) v = v
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<GOAL>ρ.invariants.carrier = ⋂ g, Function.fixedPoints ⇑(ρ g)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>ρ.IsTrivial<GOAL>ρ.invariants = ⊤
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<VAR>v : V<GOAL>ρ.averageMap v ∈ ρ.invariants
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<VAR>v : V<VAR>hv : v ∈ ρ.invariants<GOAL>ρ.averageMap v = v
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>CommSemiring k<VAR>Group G<VAR>AddCommMonoid V<VAR>Module k V<VAR>ρ : Representation k G V<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<GOAL>LinearMap.IsProj ρ.invariants ρ.averageMap
<VAR>k : Type u<VAR>CommRing k<VAR>G : Grp<VAR>X Y : Rep k ↑G<VAR>f : ↑X.V →ₗ[k] ↑Y.V<VAR>g : ↑G<GOAL>((X.ρ.linHom Y.ρ) g) f = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
<VAR>k : Type u<VAR>CommRing k<VAR>G : Grp<VAR>X Y : Rep k ↑G<VAR>f : X ⟶ Y<GOAL>↑((Representation.linHom.invariantsEquivRepHom X Y).symm f) = f.hom
<VAR>k : Type u<VAR>CommRing k<VAR>G : Grp<VAR>X Y : Rep k ↑G<VAR>f : ↥(X.ρ.linHom Y.ρ).invariants<GOAL>((Representation.linHom.invariantsEquivRepHom X Y) f).hom = ↑f
<VAR>n : ℕ<GOAL>bernoulli' n = 1 - ∑ k : Fin n, ↑(n.choose ↑k) / (↑n - ↑↑k + 1) * bernoulli' ↑k
<VAR>n : ℕ<GOAL>bernoulli' n = 1 - ∑ k ∈ Finset.range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k
<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range n.succ, ↑(n.choose (n - k)) / (↑n - ↑k + 1) * bernoulli' k = 1
<VAR>n : ℕ<GOAL>∑ k ∈ Finset.antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1
<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range n, ↑(n.choose k) * bernoulli' k = ↑n
<VAR>A : Type u_1<VAR>CommRing A<VAR>Algebra ℚ A<GOAL>bernoulli'PowerSeries A * (PowerSeries.exp A - 1) = PowerSeries.X * PowerSeries.exp A
<VAR>n : ℕ<VAR>h_odd : Odd n<VAR>hlt : 1 < n<GOAL>bernoulli' n = 0
<VAR>n : ℕ<GOAL>bernoulli' n = (-1) ^ n * bernoulli n
<VAR>n : ℕ<VAR>hn : n ≠ 1<GOAL>bernoulli n = bernoulli' n
<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range n, ↑(n.choose k) * bernoulli k = if n = 1 then 1 else 0
<VAR>n : ℕ<GOAL>∑ k ∈ Finset.antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = if n = 0 then 1 else 0
<VAR>A : Type u_1<VAR>CommRing A<VAR>Algebra ℚ A<GOAL>bernoulliPowerSeries A * (PowerSeries.exp A - 1) = PowerSeries.X
<VAR>n p : ℕ<GOAL>∑ k ∈ Finset.range n, ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
<VAR>n p : ℕ<GOAL>∑ k ∈ Finset.Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ Finset.range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
<VAR>n : ℕ+<VAR>K : Type u<VAR>Field K<VAR>CharZero K<VAR>ζ : K<VAR>ce : IsCyclotomicExtension {n} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)<VAR>hk : p ^ (k + 1) ≠ 2<GOAL>Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K)<VAR>hk : p ^ (k + 1) ≠ 2<GOAL>Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>hcycl : IsCyclotomicExtension {p ^ k} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ k)) K)<GOAL>Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsCyclotomicExtension {p ^ k} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑(p ^ k)) K)<GOAL>∃ u n, Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑↑u * ↑↑p ^ n
<VAR>p : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>IsCyclotomicExtension {p} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑p) K)<VAR>hodd : p ≠ 2<GOAL>Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>h : ∃ n, ∀ (k : ℕ), Ideal.map f p ≤ P ^ k → k ≤ n<GOAL>Ideal.ramificationIdx f p P = Nat.find h
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>h : ∀ (n : ℕ), ∃ k, Ideal.map f p ≤ P ^ k ∧ n < k<GOAL>Ideal.ramificationIdx f p P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>n : ℕ<VAR>hle : Ideal.map f p ≤ P ^ n<VAR>hgt : ¬Ideal.map f p ≤ P ^ (n + 1)<GOAL>Ideal.ramificationIdx f p P = n
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>n : ℕ<VAR>hgt : ¬Ideal.map f p ≤ P ^ n<GOAL>Ideal.ramificationIdx f p P < n
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Ideal S<GOAL>Ideal.ramificationIdx f ⊥ P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>h : ¬Ideal.map f p ≤ P<GOAL>Ideal.ramificationIdx f p P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>e : ℕ<VAR>he : e ≠ 0<VAR>hle : Ideal.map f p ≤ P ^ e<VAR>hnle : ¬Ideal.map f p ≤ P ^ (e + 1)<GOAL>Ideal.ramificationIdx f p P ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>n : ℕ<VAR>hn : n ≤ Ideal.ramificationIdx f p P<GOAL>Ideal.map f p ≤ P ^ n
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<GOAL>Ideal.map f p ≤ P ^ Ideal.ramificationIdx f p P
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<GOAL>p ≤ Ideal.comap f (P ^ Ideal.ramificationIdx f p P)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>h : Ideal.ramificationIdx f p P ≠ 0<GOAL>p ≤ Ideal.comap f P
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>IsDedekindDomain S<VAR>hp0 : Ideal.map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>hP0 : P ≠ ⊥<GOAL>Ideal.ramificationIdx f p P = Multiset.count P (UniqueFactorizationMonoid.normalizedFactors (Ideal.map f p))
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>IsDedekindDomain S<VAR>hp0 : Ideal.map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>hP0 : P ≠ ⊥<GOAL>Ideal.ramificationIdx f p P = Multiset.count P (UniqueFactorizationMonoid.factors (Ideal.map f p))
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>IsDedekindDomain S<VAR>hp0 : Ideal.map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>le : Ideal.map f p ≤ P<GOAL>Ideal.ramificationIdx f p P ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hp : p.IsMaximal<VAR>hQ : Subsingleton (S ⧸ P)<GOAL>Ideal.inertiaDeg f p P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>Algebra R S<VAR>Algebra (R ⧸ p) (S ⧸ P)<VAR>IsScalarTower R (R ⧸ p) (S ⧸ P)<VAR>hp : p.IsMaximal<GOAL>Ideal.inertiaDeg (algebraMap R S) p P = FiniteDimensional.finrank (R ⧸ p) (S ⧸ P)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>K : Type u_1<VAR>Field K<VAR>Algebra R K<VAR>hRK : IsFractionRing R K<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>AddCommGroup V<VAR>Module R V<VAR>Module K V<VAR>IsScalarTower R K V<VAR>AddCommGroup V'<VAR>Module R V'<VAR>Module S V'<VAR>IsScalarTower R S V'<VAR>AddCommGroup V''<VAR>Module R V''<VAR>IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>hb' : LinearIndependent S (⇑f' ∘ b)<GOAL>LinearIndependent K (⇑f ∘ b)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>p : Ideal R<VAR>Algebra R S<VAR>K : Type u_1<VAR>Field K<VAR>Algebra R K<VAR>L : Type u_2<VAR>Field L<VAR>Algebra S L<VAR>IsFractionRing S L<VAR>IsDomain R<VAR>IsDomain S<VAR>Algebra K L<VAR>IsNoetherian R S<VAR>Algebra R L<VAR>IsScalarTower R S L<VAR>IsScalarTower R K L<VAR>IsIntegralClosure S R L<VAR>NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p) = ⊤<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>p : Ideal R<VAR>Algebra R S<VAR>K : Type u_1<VAR>Field K<VAR>Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>Field L<VAR>Algebra S L<VAR>IsFractionRing S L<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>Algebra K L<VAR>Algebra R L<VAR>IsScalarTower R K L<VAR>IsScalarTower R S L<VAR>IsIntegralClosure S R L<VAR>hp : p.IsMaximal<VAR>IsNoetherian R S<GOAL>FiniteDimensional.finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = FiniteDimensional.finrank K L
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>x : R<GOAL>(algebraMap (R ⧸ p) (S ⧸ P ^ Ideal.ramificationIdx f p P)) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk (P ^ Ideal.ramificationIdx f p P)) (f x)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero (Ideal.ramificationIdx f p P)<VAR>x : R<GOAL>(algebraMap (R ⧸ p) (S ⧸ P)) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk P) (f x)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>i : ℕ<VAR>x : ↥(Ideal.map (Ideal.Quotient.mk (P ^ Ideal.ramificationIdx f p P)) (P ^ (i + 1)))<GOAL>↑((Ideal.powQuotSuccInclusion f p P i) x) = ↑x
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>i : ℕ<GOAL>Function.Injective ⇑(Ideal.powQuotSuccInclusion f p P i)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>i : ℕ<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>x : S<GOAL>Ideal.quotientToQuotientRangePowQuotSuccAux f p P a_mem (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(Ideal.Quotient.mk (P ^ Ideal.ramificationIdx f p P)) (a * x), ⋯⟩
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero (Ideal.ramificationIdx f p P)<VAR>i : ℕ<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>x : S<GOAL>(Ideal.quotientToQuotientRangePowQuotSucc f p P a_mem) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(Ideal.Quotient.mk (P ^ Ideal.ramificationIdx f p P)) (a * x), ⋯⟩
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero (Ideal.ramificationIdx f p P)<VAR>IsDedekindDomain S<VAR>P.IsPrime<VAR>i : ℕ<VAR>hi : i < Ideal.ramificationIdx f p P<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<GOAL>Function.Injective ⇑(Ideal.quotientToQuotientRangePowQuotSucc f p P a_mem)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero (Ideal.ramificationIdx f p P)<VAR>IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>i : ℕ<VAR>hi : i < Ideal.ramificationIdx f p P<VAR>a : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<GOAL>Function.Surjective ⇑(Ideal.quotientToQuotientRangePowQuotSucc f p P a_mem)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero (Ideal.ramificationIdx f p P)<VAR>IsDedekindDomain S<VAR>p.IsMaximal<VAR>P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>i : ℕ<VAR>hi : i < Ideal.ramificationIdx f p P<GOAL>Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ Ideal.ramificationIdx f p P)) (P ^ i)) = Module.rank (R ⧸ p) (S ⧸ P) + Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ Ideal.ramificationIdx f p P)) (P ^ (i + 1)))
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero (Ideal.ramificationIdx f p P)<VAR>IsDedekindDomain S<VAR>p.IsMaximal<VAR>P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>i : ℕ<VAR>hi : i ≤ Ideal.ramificationIdx f p P<GOAL>Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ Ideal.ramificationIdx f p P)) (P ^ i)) = (Ideal.ramificationIdx f p P - i) • Module.rank (R ⧸ p) (S ⧸ P)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>IsDedekindDomain S<VAR>p.IsMaximal<VAR>P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>he : Ideal.ramificationIdx f p P ≠ 0<GOAL>Module.rank (R ⧸ p) (S ⧸ P ^ Ideal.ramificationIdx f p P) = Ideal.ramificationIdx f p P • Module.rank (R ⧸ p) (S ⧸ P)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>p.IsMaximal<VAR>P.IsPrime<VAR>he : Ideal.ramificationIdx f p P ≠ 0<GOAL>FiniteDimensional.finrank (R ⧸ p) (S ⧸ P ^ Ideal.ramificationIdx f p P) = Ideal.ramificationIdx f p P * FiniteDimensional.finrank (R ⧸ p) (S ⧸ P)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>p : Ideal R<VAR>IsDedekindDomain S<VAR>Algebra R S<VAR>P : { x // x ∈ (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset }<GOAL>↑P ≠ ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>p : Ideal R<VAR>IsDedekindDomain S<VAR>Algebra R S<VAR>P : { x // x ∈ (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset }<GOAL>Ideal.ramificationIdx (algebraMap R S) p ↑P ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>p : Ideal R<VAR>IsDedekindDomain S<VAR>Algebra R S<VAR>p.IsMaximal<VAR>P : { x // x ∈ (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset }<GOAL>FiniteDimensional.finrank (R ⧸ p) (S ⧸ ↑P ^ Ideal.ramificationIdx (algebraMap R S) p ↑P) = Ideal.ramificationIdx (algebraMap R S) p ↑P * Ideal.inertiaDeg (algebraMap R S) p ↑P