ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>p x : Ideal R<VAR>hp : p.IsPrime<VAR>n : ℕ<VAR>hle : x ≤ p ^ n<VAR>DecidableEq (Ideal R)<VAR>hlt : ¬x ≤ p ^ (n + 1)<GOAL>Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I J K : Ideal R<VAR>coprime : ∀ (P : Ideal R), J ≤ P → K ≤ P → ¬P.IsPrime<VAR>hJ : I ≤ J<VAR>hK : I ≤ K<GOAL>I ≤ J * K
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I P : Ideal R<VAR>hP : P.IsPrime<VAR>n : ℕ<VAR>h : I ^ n ≤ P<GOAL>I ≤ P
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I P : Ideal R<VAR>_hP : P.IsPrime<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>I ^ n ≤ P ↔ I ≤ P
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>P : Ideal R<VAR>hP : P.IsPrime<GOAL>∏ i ∈ s, f i ≤ P ↔ ∃ i ∈ s, f i ≤ P
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>prime : ∀ i ∈ s, Prime (f i)<VAR>coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j<GOAL>(s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<VAR>x : R<GOAL>(IsDedekindDomain.quotientEquivPiFactors hI) ((Ideal.Quotient.mk I) x) = fun _P => (Ideal.Quotient.mk (↑_P ^ Multiset.count (↑_P) (UniqueFactorizationMonoid.factors I))) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>P : ι → Ideal R<VAR>e : ι → ℕ<VAR>prime : ∀ i ∈ s, Prime (P i)<VAR>coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j<VAR>x : (i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i<GOAL>∃ y, ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y = x ⟨i, hi⟩
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>P : ι → Ideal R<VAR>e : ι → ℕ<VAR>prime : ∀ i ∈ s, Prime (P i)<VAR>coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j<VAR>x : { x // x ∈ s } → R<GOAL>∃ y, ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>a b : R<GOAL>Ideal.span {a} ∣ Ideal.span {b} ↔ a ∣ b
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>a : R<GOAL>Squarefree (Ideal.span {a}) ↔ Squarefree a
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>NormalizationMonoid R<VAR>a b : R<VAR>ha : a ∈ UniqueFactorizationMonoid.normalizedFactors b<GOAL>Ideal.span {a} ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {b})
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : R<GOAL>multiplicity (Ideal.span {a}) (Ideal.span {b}) = multiplicity a b
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>NormalizationMonoid R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>r d : R<VAR>hr : r ≠ 0<VAR>hd : d ∈ UniqueFactorizationMonoid.normalizedFactors r<GOAL>multiplicity d r = multiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr) ⟨d, hd⟩)) (Ideal.span {r})
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>NormalizationMonoid R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>r : R<VAR>hr : r ≠ 0<VAR>I : ↑{I | I ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})}<GOAL>multiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑I) (Ideal.span {r})
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>DecidableEq R<VAR>DecidableEq (Ideal R)<VAR>NormalizationMonoid R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>r X : R<VAR>hr : r ≠ 0<VAR>hX : Prime X<GOAL>Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) = Multiset.count (normalize X) (UniqueFactorizationMonoid.normalizedFactors r)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>DecidableEq R<VAR>DecidableEq (Ideal R)<VAR>NormalizationMonoid R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>r X : R<VAR>hr : r ≠ 0<VAR>hX₁ : normUnit X = 1<VAR>hX : Prime X<GOAL>Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) = Multiset.count X (UniqueFactorizationMonoid.normalizedFactors r)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>DecidableEq (Ideal R)<VAR>DecidableEq (Associates (Ideal R))<VAR>(p : Associates (Ideal R)) → Decidable (Irreducible p)<VAR>I J : Ideal R<VAR>hI : I ≠ 0<VAR>hJ : J.IsPrime<VAR>hJ₀ : J ≠ ⊥<GOAL>(Associates.mk J).count (Associates.mk I).factors = Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>s : Submodule K V<GOAL>FiniteDimensional.finrank K (V ⧸ s) + FiniteDimensional.finrank K ↥s = FiniteDimensional.finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>s : Submodule K V<VAR>h : s < ⊤<GOAL>FiniteDimensional.finrank K ↥s < FiniteDimensional.finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s t : Submodule K V<VAR>FiniteDimensional K ↥s<VAR>FiniteDimensional K ↥t<GOAL>FiniteDimensional.finrank K ↥(s ⊔ t) + FiniteDimensional.finrank K ↥(s ⊓ t) = FiniteDimensional.finrank K ↥s + FiniteDimensional.finrank K ↥t
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s t : Submodule K V<VAR>FiniteDimensional K ↥s<VAR>FiniteDimensional K ↥t<GOAL>FiniteDimensional.finrank K ↥(s ⊔ t) ≤ FiniteDimensional.finrank K ↥s + FiniteDimensional.finrank K ↥t
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>s t : Submodule K V<VAR>hdim : FiniteDimensional.finrank K ↥s + FiniteDimensional.finrank K ↥t = FiniteDimensional.finrank K V<VAR>hdisjoint : Disjoint s t<GOAL>s ⊔ t = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>s t : Submodule K V<VAR>hdisjoint : Disjoint s t<GOAL>FiniteDimensional.finrank K ↥s + FiniteDimensional.finrank K ↥t ≤ FiniteDimensional.finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>V₂ : Type v'<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V₂<GOAL>FiniteDimensional.finrank K ↥(LinearMap.range f) + FiniteDimensional.finrank K ↥(LinearMap.ker f) = FiniteDimensional.finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>V₂ : Type v'<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>FiniteDimensional K V<VAR>FiniteDimensional K V₂<VAR>f : V →ₗ[K] V₂<VAR>h : FiniteDimensional.finrank K V₂ < FiniteDimensional.finrank K V<GOAL>LinearMap.ker f ≠ ⊥
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>V₂ : Type v'<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>FiniteDimensional K V<VAR>FiniteDimensional K V₂<VAR>H : FiniteDimensional.finrank K V = FiniteDimensional.finrank K V₂<VAR>f : V →ₗ[K] V₂<GOAL>Function.Injective ⇑f ↔ Function.Surjective ⇑f
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>V₂ : Type v'<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>FiniteDimensional K V<VAR>FiniteDimensional K V₂<VAR>H : FiniteDimensional.finrank K V = FiniteDimensional.finrank K V₂<VAR>f : V →ₗ[K] V₂<GOAL>LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>V₂ : Type v'<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>FiniteDimensional K V<VAR>FiniteDimensional K V₂<VAR>f : V →ₗ[K] V₂<VAR>hf : Function.Injective ⇑f<VAR>hdim : FiniteDimensional.finrank K V = FiniteDimensional.finrank K V₂<VAR>x : V<GOAL>(f.linearEquivOfInjective hf hdim) x = f x
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s t : Submodule K V<VAR>FiniteDimensional K ↥t<VAR>hst : s < t<GOAL>FiniteDimensional.finrank K ↥s < FiniteDimensional.finrank K ↥t
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<GOAL>StrictMono fun s => FiniteDimensional.finrank K ↥s
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>U W : Submodule K V<VAR>h : IsCompl U W<GOAL>FiniteDimensional.finrank K ↥U + FiniteDimensional.finrank K ↥W = FiniteDimensional.finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_1<VAR>Fintype ι<VAR>FiniteDimensional K V<VAR>b : ι → V<VAR>lin_ind : LinearIndependent K b<VAR>card_eq : Fintype.card ι = FiniteDimensional.finrank K V<GOAL>Submodule.span K (Set.range b) = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>Fintype ι<VAR>b : ι → V<VAR>lin_ind : LinearIndependent K b<VAR>card_eq : Fintype.card ι = FiniteDimensional.finrank K V<GOAL>Submodule.span K (Set.range b) = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>Fintype ι<VAR>b : ι → V<VAR>lin_ind : LinearIndependent K b<VAR>card_eq : Fintype.card ι = FiniteDimensional.finrank K V<GOAL>∀ (a : V), (basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id ⋯) a)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>Fintype ι<VAR>b : ι → V<VAR>lin_ind : LinearIndependent K b<VAR>card_eq : Fintype.card ι = FiniteDimensional.finrank K V<GOAL>⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = b
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Finset V<VAR>hs : s.Nonempty<VAR>lin_ind : LinearIndependent K Subtype.val<VAR>card_eq : s.card = FiniteDimensional.finrank K V<GOAL>∀ (a : V), (finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq).repr a = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Finset V<VAR>hs : s.Nonempty<VAR>lin_ind : LinearIndependent K Subtype.val<VAR>card_eq : s.card = FiniteDimensional.finrank K V<GOAL>⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = Subtype.val
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>Nonempty ↑s<VAR>Fintype ↑s<VAR>lin_ind : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<VAR>card_eq : s.toFinset.card = FiniteDimensional.finrank K V<GOAL>∀ (a : V), (setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr a = lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>Nonempty ↑s<VAR>Fintype ↑s<VAR>lin_ind : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<VAR>card_eq : s.toFinset.card = FiniteDimensional.finrank K V<GOAL>⇑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = Subtype.val
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>A : Type u_1<VAR>Semiring A<VAR>Module A V<VAR>SMul K A<VAR>IsScalarTower K A V<VAR>h : FiniteDimensional.finrank K V = 1<GOAL>IsSimpleOrder (Submodule A V)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Ring E<VAR>Algebra F E<VAR>hr : FiniteDimensional.finrank F E = 2<GOAL>IsSimpleOrder (Subalgebra F E)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<GOAL>∃ k ≤ FiniteDimensional.finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>m : ℕ<VAR>hm : FiniteDimensional.finrank K V ≤ m<GOAL>LinearMap.ker (f ^ m) = LinearMap.ker (f ^ FiniteDimensional.finrank K V)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>m : ℕ<GOAL>LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ FiniteDimensional.finrank K V)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ p<VAR>hf' : ∀ x ∈ p, f x ∈ p := ⋯<GOAL>(LinearMap.trace R ↥p) (f.restrict hf') = (LinearMap.trace R M) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>Fintype ι<VAR>b : Basis ι R S<VAR>f : S<VAR>hf : f ≠ 0<GOAL>Associated ((Algebra.norm R) f) (∏ i : ι, Ideal.smithCoeffs b (Ideal.span {f}) ⋯ i)
<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>CommRing S<VAR>IsDomain S<VAR>F : Type u_4<VAR>Field F<VAR>Algebra F[X] S<VAR>Finite ι<VAR>Algebra F S<VAR>IsScalarTower F F[X] S<VAR>b : Basis ι F[X] S<VAR>f : S<VAR>hf : f ≠ 0<GOAL>FiniteDimensional.finrank F (S ⧸ Ideal.span {f}) = ((Algebra.norm F[X]) f).natDegree
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>self : Module.Flat R M<VAR>I : Ideal R<GOAL>I.FG → Function.Injective ⇑(TensorProduct.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(TensorProduct.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.lTensor M (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.lTensor M (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type w<VAR>AddCommGroup N<VAR>Module R N<VAR>f : Module.Flat R M<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<GOAL>Module.Flat R N
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type w<VAR>AddCommGroup N<VAR>Module R N<VAR>f : Module.Flat R M<VAR>e : N ≃ₗ[R] M<GOAL>Module.Flat R N
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>Module.Projective R M<VAR>p : (ι →₀ R) →ₗ[R] M<VAR>hp : Function.Surjective ⇑p<GOAL>Module.Flat R M
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.Injective R (CharacterModule M) ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (L : N →ₗ[R] N'), Function.Injective ⇑L → Function.Injective ⇑(LinearMap.rTensor M L)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.Flat R M ↔ Module.Baer R (CharacterModule M)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Small.{v, u} R<GOAL>Module.Flat R M ↔ Module.Injective R (CharacterModule M)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type w<VAR>AddCommGroup N<VAR>Module R N<VAR>N' : Type u_1<VAR>AddCommGroup N'<VAR>Module R N'<VAR>h : Module.Flat R M<VAR>L : N →ₗ[R] N'<VAR>hL : Function.Injective ⇑L<GOAL>Function.Injective ⇑(LinearMap.rTensor M L)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type w<VAR>AddCommGroup N<VAR>Module R N<VAR>N' : Type u_1<VAR>AddCommGroup N'<VAR>Module R N'<VAR>Module.Flat R M<VAR>L : N →ₗ[R] N'<VAR>hL : Function.Injective ⇑L<GOAL>Function.Injective ⇑(LinearMap.lTensor M L)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Small.{v, u} R<GOAL>Module.Flat R M ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (L : N →ₗ[R] N'), Function.Injective ⇑L → Function.Injective ⇑(LinearMap.rTensor M L)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Small.{v, u} R<GOAL>Module.Flat R M ↔ ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N'] (L : N →ₗ[R] N'), Function.Injective ⇑L → Function.Injective ⇑(LinearMap.lTensor M L)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Small.{v, u} R<VAR>flat : Module.Flat R M<VAR>N N' N'' : Type v<VAR>AddCommGroup N<VAR>AddCommGroup N'<VAR>AddCommGroup N''<VAR>Module R N<VAR>Module R N'<VAR>Module R N''<VAR>f : N →ₗ[R] N'<VAR>g : N' →ₗ[R] N''<VAR>exact : Function.Exact ⇑f ⇑g<GOAL>Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Small.{v, u} R<VAR>flat : Module.Flat R M<VAR>N N' N'' : Type v<VAR>AddCommGroup N<VAR>AddCommGroup N'<VAR>AddCommGroup N''<VAR>Module R N<VAR>Module R N'<VAR>Module R N''<VAR>f : N →ₗ[R] N'<VAR>g : N' →ₗ[R] N''<VAR>exact : Function.Exact ⇑f ⇑g<GOAL>Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Small.{v, u} R<GOAL>Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.lTensor M f) ⇑(LinearMap.lTensor M g)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Small.{v, u} R<GOAL>Module.Flat R M ↔ ∀ ⦃N N' N'' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Submodule R M<GOAL>S.cardQuot = Nat.card (M ⧸ S)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Infinite M<GOAL>⊥.cardQuot = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>⊤.cardQuot = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>P : Submodule R M<GOAL>P.cardQuot = 1 ↔ P = ⊤
<VAR>S : Type u_1<VAR>CommRing S<VAR>I J : Ideal S<VAR>coprime : IsCoprime I J<GOAL>Submodule.cardQuot (I * J) = Submodule.cardQuot I * Submodule.cardQuot J
<VAR>S : Type u_1<VAR>CommRing S<VAR>P : Ideal S<VAR>i : ℕ<VAR>a d d' e e' : S<VAR>a_mem : a ∈ P ^ i<VAR>e_mem : e ∈ P ^ (i + 1)<VAR>e'_mem : e' ∈ P ^ (i + 1)<VAR>h : d - d' ∈ P<GOAL>a * d + e - (a * d' + e') ∈ P ^ (i + 1)
<VAR>S : Type u_1<VAR>CommRing S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>IsDedekindDomain S<VAR>i : ℕ<VAR>a c : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>c_mem : c ∈ P ^ i<GOAL>∃ d, ∃ e ∈ P ^ (i + 1), a * d + e = c
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDedekindDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>a b : S<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>ab_mem : a * b ∈ P ^ (i + 1)<GOAL>b ∈ P
<VAR>S : Type u_1<VAR>CommRing S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>IsDedekindDomain S<VAR>i : ℕ<VAR>a d d' e e' : S<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>e_mem : e ∈ P ^ (i + 1)<VAR>e'_mem : e' ∈ P ^ (i + 1)<VAR>h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)<GOAL>d - d' ∈ P
<VAR>S : Type u_1<VAR>CommRing S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>IsDedekindDomain S<VAR>i : ℕ<GOAL>Submodule.cardQuot (P ^ i) = Submodule.cardQuot P ^ i
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I J : Ideal S<GOAL>Submodule.cardQuot (I * J) = Submodule.cardQuot I * Submodule.cardQuot J
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I : Ideal S<GOAL>Ideal.absNorm I = Submodule.cardQuot I
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<GOAL>Ideal.absNorm ⊥ = 0
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<GOAL>Ideal.absNorm ⊤ = 1
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I : Ideal S<GOAL>Ideal.absNorm I = 1 ↔ I = ⊤
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I : Ideal S<GOAL>Ideal.absNorm I ≠ 0 ↔ Finite (S ⧸ I)
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>EquivLike E S ↥I<VAR>AddEquivClass E S ↥I<VAR>e : E<GOAL>(LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = Ideal.absNorm I
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>Module.Finite ℤ S<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι ℤ S<VAR>I : Ideal S<VAR>bI : Basis ι ℤ ↥I<GOAL>(b.det (Subtype.val ∘ ⇑bI)).natAbs = Ideal.absNorm I
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>Module.Finite ℤ S<VAR>r : S<GOAL>Ideal.absNorm (Ideal.span {r}) = ((Algebra.norm ℤ) r).natAbs
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I J : Ideal S<VAR>h : J ≤ I<GOAL>Ideal.absNorm I ∣ Ideal.absNorm J
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>Module.Finite ℤ S<VAR>I : Ideal S<VAR>x : S<VAR>h : x ∈ I<GOAL>↑(Ideal.absNorm I) ∣ (Algebra.norm ℤ) x
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>Module.Finite ℤ S<VAR>r : S<VAR>s : Set S<GOAL>Ideal.absNorm (Ideal.span (insert r s)) ∣ gcd (Ideal.absNorm (Ideal.span s)) ((Algebra.norm ℤ) r).natAbs
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>Module.Finite ℤ S<VAR>I : Ideal S<GOAL>Ideal.absNorm I = 0 ↔ I = ⊥
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>Module.Finite ℤ S<VAR>I : ↥(Ideal S)⁰<GOAL>Ideal.absNorm ↑I ≠ 0
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I : Ideal S<VAR>hI : Irreducible (Ideal.absNorm I)<GOAL>Irreducible I
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I : Ideal S<VAR>hI : Irreducible (Ideal.absNorm I)<GOAL>I.IsPrime
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>a : S<VAR>ha : a ≠ 0<VAR>hI : Irreducible (Ideal.absNorm (Ideal.span {a}))<GOAL>Prime a
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I : Ideal S<GOAL>↑(Ideal.absNorm I) ∈ I
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I : Ideal S<GOAL>Ideal.span {↑(Ideal.absNorm I)} ≤ I