ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a : CliffordAlgebra Q<GOAL>CliffordAlgebra.involute (CliffordAlgebra.involute a) = a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a : CliffordAlgebra Q<GOAL>CliffordAlgebra.involuteEquiv a = CliffordAlgebra.involute a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a : CliffordAlgebra Q<GOAL>CliffordAlgebra.involuteEquiv.symm a = CliffordAlgebra.involute a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>CliffordAlgebra.reverseOp ((CliffordAlgebra.ι Q) m) = MulOpposite.op ((CliffordAlgebra.ι Q) m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a : CliffordAlgebra Q<GOAL>CliffordAlgebra.reverseOpEquiv a = CliffordAlgebra.reverseOp a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>AlgEquiv.opComm CliffordAlgebra.reverseOpEquiv = CliffordAlgebra.reverseOpEquiv.symm
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<GOAL>MulOpposite.unop (CliffordAlgebra.reverseOp x) = CliffordAlgebra.reverse x
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<GOAL>MulOpposite.op (CliffordAlgebra.reverse x) = CliffordAlgebra.reverseOp x
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>CliffordAlgebra.reverse ((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι Q) m
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>r : R<GOAL>CliffordAlgebra.reverse ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>CliffordAlgebra.reverse 1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a b : CliffordAlgebra Q<GOAL>CliffordAlgebra.reverse (a * b) = CliffordAlgebra.reverse b * CliffordAlgebra.reverse a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>Function.Involutive ⇑CliffordAlgebra.reverse
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>CliffordAlgebra.reverse ∘ₗ CliffordAlgebra.reverse = LinearMap.id
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a : CliffordAlgebra Q<GOAL>CliffordAlgebra.reverse (CliffordAlgebra.reverse a) = a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>∀ (a : CliffordAlgebra Q), CliffordAlgebra.reverseEquiv a = CliffordAlgebra.reverse a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>∀ (a : CliffordAlgebra Q), CliffordAlgebra.reverseEquiv.symm a = CliffordAlgebra.reverse a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>CliffordAlgebra.reverse ∘ₗ CliffordAlgebra.involute.toLinearMap = CliffordAlgebra.involute.toLinearMap ∘ₗ CliffordAlgebra.reverse
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>Function.Commute ⇑CliffordAlgebra.reverse ⇑CliffordAlgebra.involute
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>a : CliffordAlgebra Q<GOAL>CliffordAlgebra.reverse (CliffordAlgebra.involute a) = CliffordAlgebra.involute (CliffordAlgebra.reverse a)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>l : List M<GOAL>CliffordAlgebra.reverse (List.map (⇑(CliffordAlgebra.ι Q)) l).prod = (List.map (⇑(CliffordAlgebra.ι Q)) l).reverse.prod
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>l : List M<GOAL>CliffordAlgebra.involute (List.map (⇑(CliffordAlgebra.ι Q)) l).prod = (-1) ^ l.length • (List.map (⇑(CliffordAlgebra.ι Q)) l).prod
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>p : Submodule R (CliffordAlgebra Q)<GOAL>Submodule.map CliffordAlgebra.involute.toLinearMap p = Submodule.comap CliffordAlgebra.involute.toLinearMap p
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>Submodule.map CliffordAlgebra.involute.toLinearMap (LinearMap.range (CliffordAlgebra.ι Q)) = LinearMap.range (CliffordAlgebra.ι Q)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>Submodule.comap CliffordAlgebra.involute.toLinearMap (LinearMap.range (CliffordAlgebra.ι Q)) = LinearMap.range (CliffordAlgebra.ι Q)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>n : ZMod 2<GOAL>Submodule.map CliffordAlgebra.involute.toLinearMap (CliffordAlgebra.evenOdd Q n) = CliffordAlgebra.evenOdd Q n
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>n : ZMod 2<GOAL>Submodule.comap CliffordAlgebra.involute.toLinearMap (CliffordAlgebra.evenOdd Q n) = CliffordAlgebra.evenOdd Q n
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>p : Submodule R (CliffordAlgebra Q)<GOAL>Submodule.map CliffordAlgebra.reverse p = Submodule.comap CliffordAlgebra.reverse p
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>Submodule.map CliffordAlgebra.reverse (LinearMap.range (CliffordAlgebra.ι Q)) = LinearMap.range (CliffordAlgebra.ι Q)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>Submodule.comap CliffordAlgebra.reverse (LinearMap.range (CliffordAlgebra.ι Q)) = LinearMap.range (CliffordAlgebra.ι Q)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>p q : Submodule R (CliffordAlgebra Q)<GOAL>Submodule.map CliffordAlgebra.reverse (p * q) = Submodule.map CliffordAlgebra.reverse q * Submodule.map CliffordAlgebra.reverse p
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>p q : Submodule R (CliffordAlgebra Q)<GOAL>Submodule.comap CliffordAlgebra.reverse (p * q) = Submodule.comap CliffordAlgebra.reverse q * Submodule.comap CliffordAlgebra.reverse p
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>p : Submodule R (CliffordAlgebra Q)<VAR>n : ℕ<GOAL>Submodule.map CliffordAlgebra.reverse (p ^ n) = Submodule.map CliffordAlgebra.reverse p ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>p : Submodule R (CliffordAlgebra Q)<VAR>n : ℕ<GOAL>Submodule.comap CliffordAlgebra.reverse (p ^ n) = Submodule.comap CliffordAlgebra.reverse p ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>n : ZMod 2<GOAL>Submodule.map CliffordAlgebra.reverse (CliffordAlgebra.evenOdd Q n) = CliffordAlgebra.evenOdd Q n
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>n : ZMod 2<GOAL>Submodule.comap CliffordAlgebra.reverse (CliffordAlgebra.evenOdd Q n) = CliffordAlgebra.evenOdd Q n
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<VAR>n : ZMod 2<GOAL>CliffordAlgebra.involute x ∈ CliffordAlgebra.evenOdd Q n ↔ x ∈ CliffordAlgebra.evenOdd Q n
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<VAR>n : ZMod 2<GOAL>CliffordAlgebra.reverse x ∈ CliffordAlgebra.evenOdd Q n ↔ x ∈ CliffordAlgebra.evenOdd Q n
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<VAR>h : x ∈ CliffordAlgebra.evenOdd Q 0<GOAL>CliffordAlgebra.involute x = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<VAR>h : x ∈ CliffordAlgebra.evenOdd Q 1<GOAL>CliffordAlgebra.involute x = -x
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module ℂ M<VAR>FiniteDimensional ℂ M<VAR>Q : QuadraticForm ℂ M<VAR>hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)<GOAL>QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℂ 1)
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module ℂ M<VAR>FiniteDimensional ℂ M<VAR>Q₁ Q₂ : QuadraticForm ℂ M<VAR>hQ₁ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₁)<VAR>hQ₂ : LinearMap.SeparatingLeft (QuadraticMap.associated Q₂)<GOAL>QuadraticMap.Equivalent Q₁ Q₂
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I • J = I * J
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<GOAL>r ∈ Module.annihilator R M ↔ ∀ (m : M), r • m = 0
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Injective ⇑f<GOAL>Module.annihilator R M' ≤ Module.annihilator R M
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑f<GOAL>Module.annihilator R M ≤ Module.annihilator R M'
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>e : M ≃ₗ[R] M'<GOAL>Module.annihilator R M = Module.annihilator R M'
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⊤.annihilator = Module.annihilator R M
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>r ∈ N.annihilator ↔ N ≤ Submodule.comap (r • LinearMap.id) ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>r : R<GOAL>r ∈ (Submodule.span R s).annihilator ↔ ∀ (n : ↑s), r • ↑n = 0
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>g : M<VAR>r : R<GOAL>r ∈ (Submodule.span R {g}).annihilator ↔ r • g = 0
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⊥.annihilator = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>N.annihilator = ⊤ ↔ N = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N P : Submodule R M<VAR>h : N ≤ P<GOAL>P.annihilator ≤ N.annihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort w<VAR>f : ι → Submodule R M<GOAL>(⨆ i, f i).annihilator = ⨅ i, (f i).annihilator
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>r : R<VAR>n : M<VAR>hr : r ∈ I<VAR>hn : n ∈ N<GOAL>r • n ∈ I • N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N P : Submodule R M<GOAL>I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<GOAL>↑I • N = I • N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>p : M → Prop<VAR>x : M<VAR>H : x ∈ I • N<VAR>smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)<VAR>add : ∀ (x y : M), p x → p y → p (x + y)<GOAL>p x
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>x : M<VAR>hx : x ∈ I • N<VAR>p : (x : M) → x ∈ I • N → Prop<VAR>smul : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯<VAR>add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯<GOAL>p x hx
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>m x : M<GOAL>x ∈ I • Submodule.span R {m} ↔ ∃ y ∈ I, y • m = x
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<GOAL>I • N ≤ N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>hij : I ≤ J<VAR>hnp : N ≤ P<GOAL>I • N ≤ J • P
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<VAR>h : I ≤ J<GOAL>I • N ≤ J • N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N P : Submodule R M<VAR>h : N ≤ P<GOAL>I • N ≤ I • P
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>f : R →ₗ[R] M<GOAL>Submodule.map f I ≤ I • ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>N.annihilator • N = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>Submodule.annihilator I * I = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I * Submodule.annihilator I = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<GOAL>I • ⊥ = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>⊥ • N = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>⊤ • N = N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N P : Submodule R M<GOAL>I • (N ⊔ P) = I • N ⊔ I • P
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<GOAL>(I ⊔ J) • N = I • N ⊔ J • N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<GOAL>(I • J) • N = I • J • N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>M₁ M₂ : Submodule R M<GOAL>I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_4<VAR>I : Ideal R<VAR>t : ι → Submodule R M<GOAL>I • iSup t = ⨆ i, I • t i
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_4<VAR>I : Ideal R<VAR>t : ι → Submodule R M<GOAL>I • iInf t ≤ ⨅ i, I • t i
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Set R<VAR>T : Set M<GOAL>Ideal.span S • Submodule.span R T = Submodule.span R (⋃ s ∈ S, ⋃ t ∈ T, {s • t})
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<VAR>N : Submodule R M<GOAL>Ideal.span {r} • N = r • N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>H : ∀ (r : ↑s), ↑r • x ∈ M'<GOAL>x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M'<GOAL>x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>M' : Type w<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<GOAL>Submodule.map f (I • N) = I • Submodule.map f N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type w<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>r : R<VAR>N : Submodule R M<VAR>f : M →ₗ[R] M'<GOAL>Submodule.map f (r • N) = r • Submodule.map f N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>s : Set M<VAR>x : M<GOAL>x ∈ I • Submodule.span R s ↔ x ∈ Submodule.span R (⋃ a ∈ I, ⋃ b ∈ s, {a • b})
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>ι : Type u_4<VAR>f : ι → M<VAR>x : M<GOAL>x ∈ I • Submodule.span R (Set.range f) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • f i) = x
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>ι : Type u_4<VAR>s : Set ι<VAR>f : ι → M<VAR>x : M<GOAL>x ∈ I • Submodule.span R (f '' s) ↔ ∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ I), (a.sum fun i c => c • f ↑i) = x
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>x : ↥N<GOAL>x ∈ I • ⊤ ↔ ↑x ∈ I • N
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type w<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>S : Submodule R M'<VAR>I : Ideal R<GOAL>I • Submodule.comap f S ≤ Submodule.comap f (I • S)
<VAR>R : Type u<VAR>Semiring R<VAR>I J : Ideal R<GOAL>I + J = I ⊔ J
<VAR>R : Type u<VAR>Semiring R<GOAL>0 = ⊥
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → Ideal R<GOAL>s.sum f = s.sup f
<VAR>R : Type u<VAR>CommSemiring R<GOAL>1 = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>r s : R<VAR>hr : r ∈ I<VAR>hs : s ∈ J<GOAL>r * s ∈ I * J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>r s : R<VAR>hr : r ∈ I<VAR>hs : s ∈ J<GOAL>s * r ∈ I * J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>x : R<VAR>hx : x ∈ I<VAR>n : ℕ<GOAL>x ^ n ∈ I ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>I : ι → Ideal R<VAR>x : ι → R<GOAL>(∀ i ∈ s, x i ∈ I i) → ∏ i ∈ s, x i ∈ ∏ i ∈ s, I i
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<GOAL>I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I * J ≤ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I * J ≤ I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I ⊔ I * J = I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I ⊔ J * I = I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I * J ⊔ I = I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>J * I ⊔ I = I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I * J = J * I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<GOAL>I * J * K = I * (J * K)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S T : Set R<GOAL>Ideal.span S * Ideal.span T = Ideal.span (⋃ s ∈ S, ⋃ t ∈ T, {s * t})
<VAR>R : Type u<VAR>CommSemiring R<VAR>S T : Set R<GOAL>Ideal.span S * Ideal.span T = Ideal.span (S * T)
<VAR>R : Type u<VAR>CommSemiring R<VAR>r s : R<GOAL>Ideal.span {r} * Ideal.span {s} = Ideal.span {r * s}
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : R<VAR>n : ℕ<GOAL>Ideal.span {s} ^ n = Ideal.span {s ^ n}
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>I : Ideal R<GOAL>x ∈ I * Ideal.span {y} ↔ ∃ z ∈ I, z * y = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>I : Ideal R<GOAL>x ∈ Ideal.span {y} * I ↔ ∃ z ∈ I, y * z = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<VAR>I J : Ideal R<GOAL>I ≤ Ideal.span {x} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<VAR>I J : Ideal R<GOAL>Ideal.span {x} * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>I J : Ideal R<GOAL>Ideal.span {x} * I ≤ Ideal.span {y} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>Ideal.span {x} * I ≤ Ideal.span {x} * J ↔ I ≤ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>I * Ideal.span {x} ≤ J * Ideal.span {x} ↔ I ≤ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>Ideal.span {x} * I = Ideal.span {x} * J ↔ I = J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>I * Ideal.span {x} = J * Ideal.span {x} ↔ I = J
<VAR>R : Type u<VAR>CommSemiring R<VAR>IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>Function.Injective fun x_1 => Ideal.span {x} * x_1
<VAR>R : Type u<VAR>CommSemiring R<VAR>IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>Function.Injective fun I => I * Ideal.span {x}
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<VAR>I J : Ideal R<GOAL>I = Ideal.span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<VAR>I J : Ideal R<GOAL>Ideal.span {x} * I = Ideal.span {y} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>I : ι → Set R<GOAL>∏ i ∈ s, Ideal.span (I i) = Ideal.span (∏ i ∈ s, I i)
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>I : ι → R<GOAL>∏ i ∈ s, Ideal.span {I i} = Ideal.span {∏ i ∈ s, I i}
<VAR>R : Type u<VAR>CommSemiring R<VAR>m : Multiset R<GOAL>(Multiset.map (fun x => Ideal.span {x}) m).prod = Ideal.span {m.prod}
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>I : ι → R<VAR>hI : (↑s).Pairwise (IsCoprime on I)<GOAL>(s.inf fun i => Ideal.span {I i}) = Ideal.span {∏ i ∈ s, I i}
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Type u_2<VAR>Fintype ι<VAR>I : ι → R<VAR>hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)<GOAL>⨅ i, Ideal.span {I i} = Ideal.span {∏ i : ι, I i}
<VAR>R : Type u_2<VAR>CommRing R<VAR>ι : Type u_3<VAR>Fintype ι<VAR>I : ι → ℕ<VAR>hI : Pairwise fun i j => (I i).Coprime (I j)<GOAL>⨅ i, Ideal.span {↑(I i)} = Ideal.span {↑(∏ i : ι, I i)}
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x y : R<GOAL>Ideal.span {x} ⊔ Ideal.span {y} = ⊤ ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I * J ≤ I ⊓ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Multiset (Ideal R)<GOAL>s.prod ≤ s.inf
<VAR>R : Type u<VAR>ι : Type u_1<VAR>CommSemiring R<VAR>s : Finset ι<VAR>f : ι → Ideal R<GOAL>s.prod f ≤ s.inf f
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>h : I ⊔ J = ⊤<GOAL>I * J = I ⊓ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<VAR>h : I ⊔ J = ⊤<GOAL>I ⊔ J * K = I ⊔ K
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<VAR>h : I ⊔ K = ⊤<GOAL>I ⊔ J * K = I ⊔ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<VAR>h : I ⊔ J = ⊤<GOAL>I * K ⊔ J = K ⊔ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<VAR>h : K ⊔ J = ⊤<GOAL>I * K ⊔ J = I ⊔ J
<VAR>R : Type u<VAR>ι : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>s : Finset ι<VAR>J : ι → Ideal R<VAR>h : ∀ i ∈ s, I ⊔ J i = ⊤<GOAL>I ⊔ ∏ i ∈ s, J i = ⊤
<VAR>R : Type u<VAR>ι : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>s : Finset ι<VAR>J : ι → Ideal R<VAR>h : ∀ i ∈ s, I ⊔ J i = ⊤<GOAL>I ⊔ ⨅ i ∈ s, J i = ⊤
<VAR>R : Type u<VAR>ι : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>s : Finset ι<VAR>J : ι → Ideal R<VAR>h : ∀ i ∈ s, J i ⊔ I = ⊤<GOAL>(∏ i ∈ s, J i) ⊔ I = ⊤
<VAR>R : Type u<VAR>ι : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>s : Finset ι<VAR>J : ι → Ideal R<VAR>h : ∀ i ∈ s, J i ⊔ I = ⊤<GOAL>(⨅ i ∈ s, J i) ⊔ I = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>n : ℕ<VAR>h : I ⊔ J = ⊤<GOAL>I ⊔ J ^ n = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>n : ℕ<VAR>h : I ⊔ J = ⊤<GOAL>I ^ n ⊔ J = ⊤