ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>m n : ℕ<VAR>h : I ⊔ J = ⊤<GOAL>I ^ m ⊔ J ^ n = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I * ⊥ = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>⊥ * I = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I * ⊤ = I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>⊤ * I = I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K L : Ideal R<VAR>hik : I ≤ K<VAR>hjl : J ≤ L<GOAL>I * J ≤ K * L
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<VAR>h : I ≤ J<GOAL>I * K ≤ J * K
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<VAR>h : J ≤ K<GOAL>I * J ≤ I * K
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<GOAL>I * (J ⊔ K) = I * J ⊔ I * K
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J K : Ideal R<GOAL>(I ⊔ J) * K = I * K ⊔ J * K
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>I ^ n ≤ I ^ m
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>I ^ n ≤ I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>e : I ≤ J<VAR>n : ℕ<GOAL>I ^ n ≤ J ^ n
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>I J : Ideal R<GOAL>I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>s : Multiset (Ideal R)<GOAL>s.prod = ⊥ ↔ ⊥ ∈ s
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>s : Multiset (Ideal R)<GOAL>s.prod = ⊥ ↔ ∃ I ∈ s, I = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>w x y z : R<GOAL>Ideal.span {w, x} * Ideal.span {y, z} = Ideal.span {w * y, w * z, x * y, x * z}
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>IsCoprime I J ↔ Codisjoint I J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>IsCoprime I J ↔ I + J = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>IsCoprime I J ↔ I ⊔ J = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>[IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>h : IsCoprime I J<GOAL>Codisjoint I J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>h : IsCoprime I J<GOAL>I + J = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>h : IsCoprime I J<GOAL>∃ i ∈ I, ∃ j ∈ J, i + j = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>h : IsCoprime I J<GOAL>I ⊔ J = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>I ⊓ J = I * J
<VAR>R : Type u<VAR>CommSemiring R<VAR>x y : R<GOAL>IsCoprime (Ideal.span {x}) (Ideal.span {y}) ↔ IsCoprime x y
<VAR>R : Type u<VAR>ι : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>J : ι → Ideal R<VAR>s : Finset ι<VAR>hf : ∀ j ∈ s, IsCoprime I (J j)<GOAL>IsCoprime I (⨅ j ∈ s, J j)
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>r : R<GOAL>r ∈ I.radical ↔ ∃ n, r ^ n ∈ I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I ≤ I.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I.radical = I ↔ I.IsRadical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>k : ℕ<VAR>hk : 1 < k<GOAL>I.IsRadical ↔ ∀ (r : R), r ^ k ∈ I → r ∈ I
<VAR>R : Type u<VAR>CommSemiring R<GOAL>⊤.radical = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>H : I ≤ J<GOAL>I.radical ≤ J.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I.radical.IsRadical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I.radical.radical = I.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>hJ : J.IsRadical<GOAL>I.radical ≤ J ↔ I ≤ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>I.radical ≤ J.radical ↔ I ≤ J.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I.radical = ⊤ ↔ I = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>H : I.IsPrime<GOAL>I.IsRadical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>H : I.IsPrime<GOAL>I.radical = I
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>x : R<VAR>m : ℕ<VAR>hx : x ^ m ∈ I.radical<GOAL>x ∈ I.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>y : R<VAR>hI : I.IsRadical<GOAL>Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I.toAddSubmonoid
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>(I ⊔ J).radical = (I.radical ⊔ J.radical).radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>(I ⊓ J).radical = I.radical ⊓ J.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>hI : I.IsRadical<VAR>hJ : J.IsRadical<GOAL>(I ⊓ J).IsRadical
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Sort u_2<VAR>I : ι → Ideal R<GOAL>(⨅ i, I i).radical ≤ ⨅ i, (I i).radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι : Sort u_2<VAR>I : ι → Ideal R<VAR>hI : ∀ (i : ι), (I i).IsRadical<GOAL>(⨅ i, I i).IsRadical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<GOAL>(I * J).radical = I.radical ⊓ J.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>hJ : J.IsPrime<GOAL>I.radical ≤ J ↔ I ≤ J
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<GOAL>I.radical = sInf {J | I ≤ J ∧ J.IsPrime}
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>NoZeroDivisors R<GOAL>⊥.IsRadical
<VAR>R : Type u<VAR>CommSemiring R<VAR>NoZeroDivisors R<GOAL>⊥.radical = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>n : ℕ<GOAL>⊤ ^ n = ⊤
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>n : ℕ<GOAL>n ≠ 0 → (I ^ n).radical = I.radical
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J P : Ideal R<VAR>hp : P.IsPrime<GOAL>I * J ≤ P ↔ I ≤ P ∨ J ≤ P
<VAR>R : Type u<VAR>CommSemiring R<VAR>I J P : Ideal R<VAR>hp : P.IsPrime<GOAL>I ⊓ J ≤ P ↔ I ≤ P ∨ J ≤ P
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Multiset (Ideal R)<VAR>P : Ideal R<VAR>hp : P.IsPrime<GOAL>s.prod ≤ P ↔ ∃ I ∈ s, I ≤ P
<VAR>R : Type u<VAR>ι : Type u_1<VAR>CommSemiring R<VAR>s : Multiset ι<VAR>f : ι → Ideal R<VAR>P : Ideal R<VAR>hp : P.IsPrime<GOAL>(Multiset.map f s).prod ≤ P ↔ ∃ i ∈ s, f i ≤ P
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>s : Multiset R<GOAL>s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
<VAR>R : Type u<VAR>ι : Type u_1<VAR>CommSemiring R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>P : Ideal R<VAR>hp : P.IsPrime<GOAL>s.prod f ≤ P ↔ ∃ i ∈ s, f i ≤ P
<VAR>R : Type u<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>s : Finset R<GOAL>∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I
<VAR>R : Type u<VAR>ι : Type u_1<VAR>CommSemiring R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>P : Ideal R<VAR>hp : P.IsPrime<GOAL>s.inf f ≤ P ↔ ∃ i ∈ s, f i ≤ P
<VAR>R : Type u<VAR>Ring R<VAR>I J K : Ideal R<GOAL>↑I ⊆ ↑J ∪ ↑K ↔ I ≤ J ∨ I ≤ K
<VAR>ι : Type u_1<VAR>R : Type u<VAR>CommRing R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>a b : ι<VAR>hp : ∀ i ∈ s, (f i).IsPrime<VAR>I : Ideal R<GOAL>↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) ↔ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
<VAR>ι : Type u_1<VAR>R : Type u<VAR>CommRing R<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>a b : ι<VAR>hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime<VAR>I : Ideal R<GOAL>↑I ⊆ ⋃ i ∈ ↑s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f 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 : Ideal R<GOAL>IsUnit I ↔ I = ⊤
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>I : Ideal R<VAR>v : ι → M<VAR>f : ι →₀ ↥I<GOAL>(Ideal.finsuppTotal ι M I v) f = f.sum fun i x => ↑x • v i
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>I : Ideal R<VAR>v : ι → M<VAR>Fintype ι<VAR>f : ι →₀ ↥I<GOAL>(Ideal.finsuppTotal ι M I v) f = ∑ i : ι, ↑(f i) • v i
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_3<VAR>CommRing R<VAR>Module R M<VAR>I : Ideal R<VAR>v : ι → M<GOAL>LinearMap.range (Ideal.finsuppTotal ι M I v) = I • Submodule.span R (Set.range v)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>x : R<VAR>v : α → R<GOAL>x ∈ Ideal.span (Set.range v) ↔ ∃ c, (c.sum fun i a => a * v i) = x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>Fintype α<VAR>x : R<VAR>v : α → R<GOAL>x ∈ Ideal.span (Set.range v) ↔ ∃ c, ∑ i : α, c i * v i = x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>r : R<GOAL>Associates.mk (Ideal.span {r}) ≠ 0 ↔ r ≠ 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>NoZeroDivisors R<VAR>r : R<GOAL>Ideal.span {r} ∈ nonZeroDivisors (Ideal R) ↔ r ∈ nonZeroDivisors R
<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set R<VAR>N : Submodule R M<GOAL>Ideal.span s • N = s • N
<VAR>R : Type u<VAR>CommSemiring R<VAR>s : Set R<GOAL>s • ⊤ = Ideal.span s
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : E →ₗ[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<GOAL>LinearMap.ker (LinearMap.id - p.subtype ∘ₗ f) = p
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : E →ₗ[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<GOAL>LinearMap.range f = ⊤
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : E →ₗ[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<GOAL>IsCompl p (LinearMap.ker f)
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : ↥q<GOAL>(p.quotientEquivOfIsCompl q h).symm x = Submodule.Quotient.mk ↑x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : ↥q<GOAL>(p.quotientEquivOfIsCompl q h) (Submodule.Quotient.mk ↑x) = x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : E ⧸ p<GOAL>Submodule.Quotient.mk ↑((p.quotientEquivOfIsCompl q h) x) = x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<GOAL>↑(p.prodEquivOfIsCompl q h) = p.subtype.coprod q.subtype
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : ↥p × ↥q<GOAL>(p.prodEquivOfIsCompl q h) x = ↑x.1 + ↑x.2
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : ↥p<GOAL>(p.prodEquivOfIsCompl q h).symm ↑x = (x, 0)
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : ↥q<GOAL>(p.prodEquivOfIsCompl q h).symm ↑x = (0, x)
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : E<GOAL>((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : E<GOAL>((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ x ∈ p
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<GOAL>LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q h = q.prodEquivOfIsCompl p ⋯
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : ↥p<GOAL>(p.linearProjOfIsCompl q h) ↑x = x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<GOAL>LinearMap.range (p.linearProjOfIsCompl q h) = ⊤
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : E<GOAL>(p.linearProjOfIsCompl q h) x = 0 ↔ x ∈ q
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : E<VAR>hx : x ∈ q<GOAL>(p.linearProjOfIsCompl q h) x = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : ↥q<GOAL>(p.linearProjOfIsCompl q h) ↑x = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<GOAL>LinearMap.ker (p.linearProjOfIsCompl q h) = q
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<GOAL>p.linearProjOfIsCompl q h ∘ₗ p.subtype = LinearMap.id
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>x : E<GOAL>(p.linearProjOfIsCompl q h) ↑((p.linearProjOfIsCompl q h) x) = (p.linearProjOfIsCompl q h) x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>hc : IsCompl p q<VAR>x : E<GOAL>∃! u, ↑u.1 + ↑u.2 = x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>hc : IsCompl p q<VAR>x : E<GOAL>∃ u v, ↑u + ↑v = x ∧ ∀ (r : ↥p) (s : ↥q), ↑r + ↑s = x → r = u ∧ s = v
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p q : Submodule R E<VAR>hpq : IsCompl p q<VAR>x : E<GOAL>↑((p.linearProjOfIsCompl q hpq) x) + ↑((q.linearProjOfIsCompl p ⋯) x) = x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>φ : ↥p →ₗ[R] F<VAR>ψ : ↥q →ₗ[R] F<VAR>u : ↥p<GOAL>(LinearMap.ofIsCompl h φ ψ) ↑u = φ u
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>φ : ↥p →ₗ[R] F<VAR>ψ : ↥q →ₗ[R] F<VAR>v : ↥q<GOAL>(LinearMap.ofIsCompl h φ ψ) ↑v = ψ v
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>φ : ↥p →ₗ[R] F<VAR>ψ : ↥q →ₗ[R] F<VAR>χ : E →ₗ[R] F<VAR>hφ : ∀ (u : ↥p), φ u = χ ↑u<VAR>hψ : ∀ (u : ↥q), ψ u = χ ↑u<GOAL>LinearMap.ofIsCompl h φ ψ = χ
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>φ : ↥p →ₗ[R] F<VAR>ψ : ↥q →ₗ[R] F<VAR>χ : E →ₗ[R] F<VAR>hφ : φ = χ ∘ₗ p.subtype<VAR>hψ : ψ = χ ∘ₗ q.subtype<GOAL>LinearMap.ofIsCompl h φ ψ = χ
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>p q : Submodule R E<VAR>h : IsCompl p q<GOAL>LinearMap.ofIsCompl h 0 0 = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>φ₁ φ₂ : ↥p →ₗ[R] F<VAR>ψ₁ ψ₂ : ↥q →ₗ[R] F<GOAL>LinearMap.ofIsCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = LinearMap.ofIsCompl h φ₁ ψ₁ + LinearMap.ofIsCompl h φ₂ ψ₂
<VAR>R : Type u_7<VAR>CommRing R<VAR>E : Type u_8<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_9<VAR>AddCommGroup F<VAR>Module R F<VAR>p q : Submodule R E<VAR>h : IsCompl p q<VAR>φ : ↥p →ₗ[R] F<VAR>ψ : ↥q →ₗ[R] F<VAR>c : R<GOAL>LinearMap.ofIsCompl h (c • φ) (c • ψ) = c • LinearMap.ofIsCompl h φ ψ
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>R₁ : Type u_7<VAR>CommRing R₁<VAR>Module R₁ E<VAR>Module R₁ F<VAR>p q : Submodule R₁ E<VAR>h : IsCompl p q<VAR>φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)<GOAL>(LinearMap.ofIsComplProd h) φ = LinearMap.ofIsCompl h φ.1 φ.2
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : E →ₗ[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<GOAL>p.linearProjOfIsCompl (LinearMap.ker f) ⋯ = f
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>G : Type u_4<VAR>AddCommGroup G<VAR>Module R G<VAR>f : E →ₗ[R] F<VAR>g : E →ₗ[R] G<VAR>hf : LinearMap.range f = ⊤<VAR>hg : LinearMap.range g = ⊤<VAR>hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g)<GOAL>↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) = f.prod g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>G : Type u_4<VAR>AddCommGroup G<VAR>Module R G<VAR>f : E →ₗ[R] F<VAR>g : E →ₗ[R] G<VAR>hf : LinearMap.range f = ⊤<VAR>hg : LinearMap.range g = ⊤<VAR>hfg : IsCompl (LinearMap.ker f) (LinearMap.ker g)<VAR>x : E<GOAL>(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) x = (f x, g x)
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>q : { q // IsCompl p q }<GOAL>↑(p.isComplEquivProj q) = p.linearProjOfIsCompl ↑q ⋯
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : { f // ∀ (x : ↥p), f ↑x = x }<GOAL>↑(p.isComplEquivProj.symm f) = LinearMap.ker ↑f
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : { f // IsIdempotentElem f ∧ LinearMap.range f = p }<GOAL>↑(p.isIdempotentElemEquiv f) = LinearMap.codRestrict p ↑f ⋯
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : { f // ∀ (x : ↥p), f ↑x = x }<GOAL>↑(p.isIdempotentElemEquiv.symm f) = p.subtype ∘ₗ ↑f
<VAR>S : Type u_5<VAR>Semiring S<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>Module S M<VAR>m : Submodule S M<VAR>F : Type u_7<VAR>FunLike F M M<VAR>f : F<VAR>self : LinearMap.IsProj m f<VAR>x : M<GOAL>f x ∈ m
<VAR>S : Type u_5<VAR>Semiring S<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>Module S M<VAR>m : Submodule S M<VAR>F : Type u_7<VAR>FunLike F M M<VAR>f : F<VAR>self : LinearMap.IsProj m f<VAR>x : M<GOAL>x ∈ m → f x = x
<VAR>S : Type u_5<VAR>Semiring S<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>Module S M<VAR>f : M →ₗ[S] M<GOAL>(∃ p, LinearMap.IsProj p f) ↔ f ∘ₗ f = f
<VAR>S : Type u_5<VAR>Semiring S<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>Module S M<VAR>m : Submodule S M<VAR>f : M →ₗ[S] M<VAR>h : LinearMap.IsProj m f<VAR>x : M<GOAL>↑(h.codRestrict x) = f x
<VAR>S : Type u_5<VAR>Semiring S<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>Module S M<VAR>m : Submodule S M<VAR>f : M →ₗ[S] M<VAR>h : LinearMap.IsProj m f<VAR>x : ↥m<GOAL>h.codRestrict ↑x = x
<VAR>S : Type u_5<VAR>Semiring S<VAR>M : Type u_6<VAR>AddCommMonoid M<VAR>Module S M<VAR>m : Submodule S M<VAR>f : M →ₗ[S] M<VAR>h : LinearMap.IsProj m f<GOAL>LinearMap.ker h.codRestrict = LinearMap.ker f
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : E →ₗ[R] E<VAR>h : LinearMap.IsProj p f<GOAL>IsCompl p (LinearMap.ker f)
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : E →ₗ[R] E<VAR>h : LinearMap.IsProj p f<GOAL>f = ↑(p.prodEquivOfIsCompl (LinearMap.ker f) ⋯) ∘ₗ LinearMap.id.prodMap 0 ∘ₗ ↑(p.prodEquivOfIsCompl (LinearMap.ker f) ⋯).symm
<VAR>R : Type u_1<VAR>CommRing R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>p : Submodule R E<VAR>f : E →ₗ[R] E<VAR>h : LinearMap.IsProj p f<GOAL>f = (p.prodEquivOfIsCompl (LinearMap.ker f) ⋯).conj (LinearMap.id.prodMap 0)
<VAR>ι : Type u_4<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>LinearOrder ι<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>bm : Basis ι R M<VAR>i j : ι<GOAL>((Q.toBilin bm) (bm i)) (bm j) = if i = j then Q (bm i) else if i < j then QuadraticMap.polar (⇑Q) (bm i) (bm j) else 0
<VAR>ι : Type u_4<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>LinearOrder ι<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticMap R M N<VAR>bm : Basis ι R M<GOAL>(Q.toBilin bm).toQuadraticMap = Q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Module.Free R M<GOAL>Function.Surjective LinearMap.BilinMap.toQuadraticMap
<VAR>R : Type u_1<VAR>CommRing R<GOAL>CliffordAlgebra.ι 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : CliffordAlgebra 0<GOAL>CliffordAlgebra.reverse x = x
<VAR>R : Type u_1<VAR>CommRing R<GOAL>CliffordAlgebra.reverse = LinearMap.id
<VAR>R : Type u_1<VAR>CommRing R<GOAL>CliffordAlgebra.involute = AlgHom.id R (CliffordAlgebra 0)
<VAR>r : ℝ<GOAL>CliffordAlgebraComplex.Q r = -(r * r)
<VAR>r : ℝ<GOAL>CliffordAlgebraComplex.toComplex ((CliffordAlgebra.ι CliffordAlgebraComplex.Q) r) = r • Complex.I
<VAR>c : CliffordAlgebra CliffordAlgebraComplex.Q<GOAL>CliffordAlgebraComplex.toComplex (CliffordAlgebra.involute c) = (starRingEnd ℂ) (CliffordAlgebraComplex.toComplex c)
<GOAL>CliffordAlgebraComplex.ofComplex Complex.I = (CliffordAlgebra.ι CliffordAlgebraComplex.Q) 1
<GOAL>CliffordAlgebraComplex.toComplex.comp CliffordAlgebraComplex.ofComplex = AlgHom.id ℝ ℂ
<VAR>c : ℂ<GOAL>CliffordAlgebraComplex.toComplex (CliffordAlgebraComplex.ofComplex c) = c
<GOAL>CliffordAlgebraComplex.ofComplex.comp CliffordAlgebraComplex.toComplex = AlgHom.id ℝ (CliffordAlgebra CliffordAlgebraComplex.Q)
<VAR>c : CliffordAlgebra CliffordAlgebraComplex.Q<GOAL>CliffordAlgebraComplex.ofComplex (CliffordAlgebraComplex.toComplex c) = c
<VAR>a : CliffordAlgebra CliffordAlgebraComplex.Q<GOAL>CliffordAlgebraComplex.equiv a = CliffordAlgebraComplex.toComplex a
<VAR>a : ℂ<GOAL>CliffordAlgebraComplex.equiv.symm a = CliffordAlgebraComplex.ofComplex a
<VAR>x : CliffordAlgebra CliffordAlgebraComplex.Q<GOAL>CliffordAlgebra.reverse x = x
<VAR>c : ℂ<GOAL>CliffordAlgebraComplex.ofComplex ((starRingEnd ℂ) c) = CliffordAlgebra.involute (CliffordAlgebraComplex.ofComplex c)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>v : R × R<GOAL>(CliffordAlgebraQuaternion.Q c₁ c₂) v = c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>(CliffordAlgebraQuaternion.quaternionBasis c₁ c₂).i = (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>(CliffordAlgebraQuaternion.quaternionBasis c₁ c₂).j = (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>(CliffordAlgebraQuaternion.quaternionBasis c₁ c₂).k = (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0) * (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>v : R × R<GOAL>CliffordAlgebraQuaternion.toQuaternion ((CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) v) = { re := 0, imI := v.1, imJ := v.2, imK := 0 }
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>c : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)<GOAL>CliffordAlgebraQuaternion.toQuaternion (star c) = star (CliffordAlgebraQuaternion.toQuaternion c)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a₁ a₂ a₃ a₄ : R<GOAL>CliffordAlgebraQuaternion.ofQuaternion { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = (algebraMap R (CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂))) a₁ + a₂ • (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0) + a₃ • (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1) + a₄ • ((CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0) * (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1))
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>CliffordAlgebraQuaternion.ofQuaternion.comp CliffordAlgebraQuaternion.toQuaternion = AlgHom.id R (CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂))
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>c : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)<GOAL>CliffordAlgebraQuaternion.ofQuaternion (CliffordAlgebraQuaternion.toQuaternion c) = c
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<GOAL>CliffordAlgebraQuaternion.toQuaternion.comp CliffordAlgebraQuaternion.ofQuaternion = AlgHom.id R (QuaternionAlgebra R c₁ c₂)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>q : QuaternionAlgebra R c₁ c₂<GOAL>CliffordAlgebraQuaternion.toQuaternion (CliffordAlgebraQuaternion.ofQuaternion q) = q
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)<GOAL>CliffordAlgebraQuaternion.equiv a = CliffordAlgebraQuaternion.toQuaternion a
<VAR>R : Type u_1<VAR>CommRing R<VAR>c₁ c₂ : R<VAR>a : QuaternionAlgebra R c₁ c₂<GOAL>CliffordAlgebraQuaternion.equiv.symm a = CliffordAlgebraQuaternion.ofQuaternion a