ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup G<VAR>f : G →+ N<VAR>hf : Function.Bijective ⇑f<GOAL>AddSubgroup.map f H.normalizer = (AddSubgroup.map f H).normalizer
<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>Group G₁<VAR>Group G₂<VAR>Group G₃<VAR>f : G₁ →* G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : G₁ →* G₃<VAR>hg : f.ker ≤ g.ker<VAR>x : G₁<GOAL>(f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x
<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>AddGroup G₁<VAR>AddGroup G₂<VAR>AddGroup G₃<VAR>f : G₁ →+ G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : G₁ →+ G₃<VAR>hg : f.ker ≤ g.ker<VAR>x : G₁<GOAL>(f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x
<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>AddGroup G₁<VAR>AddGroup G₂<VAR>AddGroup G₃<VAR>f : G₁ →+ G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : { g // f.ker ≤ g.ker }<VAR>x : G₁<GOAL>((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x
<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>Group G₁<VAR>Group G₂<VAR>Group G₃<VAR>f : G₁ →* G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : { g // f.ker ≤ g.ker }<VAR>x : G₁<GOAL>((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x
<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>Group G₁<VAR>Group G₂<VAR>Group G₃<VAR>f : G₁ →* G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : { g // f.ker ≤ g.ker }<GOAL>((f.liftOfRightInverse f_inv hf) g).comp f = ↑g
<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>AddGroup G₁<VAR>AddGroup G₂<VAR>AddGroup G₃<VAR>f : G₁ →+ G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : { g // f.ker ≤ g.ker }<GOAL>((f.liftOfRightInverse f_inv hf) g).comp f = ↑g
<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>AddGroup G₁<VAR>AddGroup G₂<VAR>AddGroup G₃<VAR>f : G₁ →+ G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : G₁ →+ G₃<VAR>hg : f.ker ≤ g.ker<VAR>h : G₂ →+ G₃<VAR>hh : h.comp f = g<GOAL>h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩
<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>Group G₁<VAR>Group G₂<VAR>Group G₃<VAR>f : G₁ →* G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : G₁ →* G₃<VAR>hg : f.ker ≤ g.ker<VAR>h : G₂ →* G₃<VAR>hh : h.comp f = g<GOAL>h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩
<VAR>G : Type u_1<VAR>AddGroup G<VAR>N : Type u_5<VAR>AddGroup N<VAR>H : AddSubgroup N<VAR>hH : H.Normal<VAR>f : G →+ N<GOAL>(AddSubgroup.comap f H).Normal
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>H : Subgroup N<VAR>hH : H.Normal<VAR>f : G →* N<GOAL>(Subgroup.comap f H).Normal
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>hH : H.Normal<VAR>K : Subgroup G<GOAL>(H.subgroupOf K).Normal
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>hH : H.Normal<VAR>K : AddSubgroup G<GOAL>(H.addSubgroupOf K).Normal
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>s : Set G<VAR>f : G →* N<VAR>hf : Function.Surjective ⇑f<GOAL>Subgroup.map f (Subgroup.normalClosure s) = Subgroup.normalClosure (⇑f '' s)
<VAR>G : Type u_1<VAR>Group G<VAR>N : Type u_5<VAR>Group N<VAR>s : Set N<VAR>f : G ≃* N<GOAL>Subgroup.normalClosure (⇑f ⁻¹' s) = Subgroup.comap (↑f) (Subgroup.normalClosure s)
<VAR>G : Type u_6<VAR>H : Type u_7<VAR>Group G<VAR>Group H<VAR>φ : G →* H<VAR>hφ : Function.Injective ⇑φ<VAR>L : Subgroup G<VAR>n : (Subgroup.map φ L).Normal<GOAL>L.Normal
<VAR>G : Type u_1<VAR>Group G<VAR>K : Subgroup G<VAR>L : Subgroup ↥K<VAR>n : (Subgroup.map K.subtype L).Normal<GOAL>L.Normal
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>f : G →+ G'<VAR>H' : AddSubgroup G'<VAR>x : ↥(AddSubmonoid.comap f H'.toAddSubmonoid)<GOAL>↑((f.addSubgroupComap H') x) = f ↑x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>H' : Subgroup G'<VAR>x : ↥(Submonoid.comap f H'.toSubmonoid)<GOAL>↑((f.subgroupComap H') x) = f ↑x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>H : Subgroup G<VAR>x : ↥H.toSubmonoid<GOAL>↑((f.subgroupMap H) x) = f ↑x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>f : G →+ G'<VAR>H : AddSubgroup G<VAR>x : ↥H.toAddSubmonoid<GOAL>↑((f.addSubgroupMap H) x) = f ↑x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>f : G →+ G'<VAR>H : AddSubgroup G<GOAL>Function.Surjective ⇑(f.addSubgroupMap H)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>f : G →* G'<VAR>H : Subgroup G<GOAL>Function.Surjective ⇑(f.subgroupMap H)
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H = K<VAR>x : ↥H<GOAL>↑((MulEquiv.subgroupCongr h) x) = ↑x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H = K<VAR>x : ↥H<GOAL>↑((AddEquiv.addSubgroupCongr h) x) = ↑x
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>h : H = K<VAR>x : ↥K<GOAL>↑((AddEquiv.addSubgroupCongr h).symm x) = ↑x
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>h : H = K<VAR>x : ↥K<GOAL>↑((MulEquiv.subgroupCongr h).symm x) = ↑x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>e : G ≃+ G'<VAR>H : AddSubgroup G<VAR>g : ↥H<GOAL>↑((e.addSubgroupMap H) g) = e ↑g
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>e : G ≃* G'<VAR>H : Subgroup G<VAR>g : ↥H<GOAL>↑((e.subgroupMap H) g) = e ↑g
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>e : G ≃+ G'<VAR>H : AddSubgroup G<VAR>g : ↥(AddSubgroup.map (↑e) H)<GOAL>(e.addSubgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>e : G ≃* G'<VAR>H : Subgroup G<VAR>g : ↥(Subgroup.map (↑e) H)<GOAL>(e.subgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>AddGroup G<VAR>AddGroup G'<VAR>H : AddSubgroup G<VAR>e : G ≃+ G'<GOAL>H.equivMapOfInjective ↑e ⋯ = e.addSubgroupMap H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>Group G<VAR>Group G'<VAR>H : Subgroup G<VAR>e : G ≃* G'<GOAL>H.equivMapOfInjective ↑e ⋯ = e.subgroupMap H
<VAR>C : Type u_6<VAR>CommGroup C<VAR>s t : Subgroup C<VAR>x : C<GOAL>x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
<VAR>C : Type u_6<VAR>AddCommGroup C<VAR>s t : AddSubgroup C<VAR>x : C<GOAL>x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
<VAR>C : Type u_6<VAR>CommGroup C<VAR>s t : Subgroup C<VAR>x : C<GOAL>x ∈ s ⊔ t ↔ ∃ y z, ↑y * ↑z = x
<VAR>C : Type u_6<VAR>AddCommGroup C<VAR>s t : AddSubgroup C<VAR>x : C<GOAL>x ∈ s ⊔ t ↔ ∃ y z, ↑y + ↑z = x
<VAR>C : Type u_6<VAR>CommGroup C<VAR>x y z : C<GOAL>z ∈ Subgroup.closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z
<VAR>C : Type u_6<VAR>AddCommGroup C<VAR>x y z : C<GOAL>z ∈ AddSubgroup.closure {x, y} ↔ ∃ m n, m • x + n • y = z
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hHK : H ≤ K<GOAL>(H.subgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>hHK : H ≤ K<GOAL>(H.addSubgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k + h + -k ∈ H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>A B' B : AddSubgroup G<VAR>hB : B' ≤ B<VAR>hN : (B'.addSubgroupOf B).Normal<GOAL>((A ⊓ B').addSubgroupOf (A ⊓ B)).Normal
<VAR>G : Type u_1<VAR>Group G<VAR>A B' B : Subgroup G<VAR>hB : B' ≤ B<VAR>hN : (B'.subgroupOf B).Normal<GOAL>((A ⊓ B').subgroupOf (A ⊓ B)).Normal
<VAR>G : Type u_1<VAR>Group G<VAR>A' A : Subgroup G<VAR>B : Subgroup G<VAR>hA : A' ≤ A<VAR>hN : (A'.subgroupOf A).Normal<GOAL>((A' ⊓ B).subgroupOf (A ⊓ B)).Normal
<VAR>G : Type u_1<VAR>AddGroup G<VAR>A' A : AddSubgroup G<VAR>B : AddSubgroup G<VAR>hA : A' ≤ A<VAR>hN : (A'.addSubgroupOf A).Normal<GOAL>((A' ⊓ B).addSubgroupOf (A ⊓ B)).Normal
<VAR>G : Type u_1<VAR>AddGroup G<VAR>A A' B : AddSubgroup G<VAR>hA : A ≤ B<VAR>hA' : A' ≤ B<GOAL>(A ⊔ A').addSubgroupOf B = A.addSubgroupOf B ⊔ A'.addSubgroupOf B
<VAR>G : Type u_1<VAR>Group G<VAR>A A' B : Subgroup G<VAR>hA : A ≤ B<VAR>hA' : A' ≤ B<GOAL>(A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H K : AddSubgroup G<VAR>hK : H ≤ K<VAR>hN : (H.addSubgroupOf K).Normal<VAR>a b : G<VAR>hb : b ∈ K<VAR>h : a + b ∈ H<GOAL>b + a ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H K : Subgroup G<VAR>hK : H ≤ K<VAR>hN : (H.subgroupOf K).Normal<VAR>a b : G<VAR>hb : b ∈ K<VAR>h : a * b ∈ H<GOAL>b * a ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<VAR>hH₁ : H₁.Normal<VAR>hH₂ : H₂.Normal<VAR>hdis : Disjoint H₁ H₂<VAR>x y : G<VAR>hx : x ∈ H₁<VAR>hy : y ∈ H₂<GOAL>Commute x y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H₁ H₂ : AddSubgroup G<VAR>hH₁ : H₁.Normal<VAR>hH₂ : H₂.Normal<VAR>hdis : Disjoint H₁ H₂<VAR>x y : G<VAR>hx : x ∈ H₁<VAR>hy : y ∈ H₂<GOAL>AddCommute x y
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H₁ H₂ : AddSubgroup G<GOAL>Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<GOAL>Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H₁ H₂ : AddSubgroup G<GOAL>Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 0
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<GOAL>Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<GOAL>Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H₁ H₂ : AddSubgroup G<GOAL>Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x + y = 0 → x = 0 ∧ y = 0
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<VAR>h : Disjoint H₁ H₂<GOAL>Function.Injective fun g => ↑g.1 * ↑g.2
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H₁ H₂ : AddSubgroup G<VAR>h : Disjoint H₁ H₂<GOAL>Function.Injective fun g => ↑g.1 + ↑g.2
<VAR>G : Type u_1<VAR>Group G<VAR>N : Subgroup G<VAR>hn : N.Normal<VAR>g g' : G<VAR>hg : g ∈ N<VAR>hg' : g' ∈ N<VAR>hc : IsConj g g'<VAR>ht : Subgroup.normalClosure {⟨g, hg⟩} = ⊤<GOAL>Subgroup.normalClosure {⟨g', hg'⟩} = ⊤
<VAR>G : Type u_6<VAR>Monoid G<VAR>g : ConjClasses G<GOAL>g ∈ ConjClasses.noncenter G ↔ g.carrier.Nontrivial
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Subsemiring R<GOAL>a • S = Subsemiring.map (MulSemiringAction.toRingHom M R a) S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>m : M<VAR>S : Subsemiring R<GOAL>↑(m • S) = m • ↑S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>m : M<VAR>S : Subsemiring R<GOAL>(m • S).toAddSubmonoid = m • S.toAddSubmonoid
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>m : M<VAR>r : R<VAR>S : Subsemiring R<GOAL>r ∈ S → m • r ∈ m • S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>m : M<VAR>r : R<VAR>S : Subsemiring R<GOAL>r ∈ m • S ↔ ∃ s ∈ S, m • s = r
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<GOAL>a • ⊥ = ⊥
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Subsemiring R<GOAL>a • (S ⊔ T) = a • S ⊔ a • T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>s : Set R<GOAL>a • Subsemiring.closure s = Subsemiring.closure (a • s)
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Subsemiring R<VAR>x : R<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Subsemiring R<VAR>x : R<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Subsemiring R<VAR>x : R<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Subsemiring R<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Subsemiring R<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Subsemiring R<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S : Subsemiring R<VAR>x : R<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S : Subsemiring R<VAR>x : R<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S : Subsemiring R<VAR>x : R<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S T : Subsemiring R<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S T : Subsemiring R<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S T : Subsemiring R<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>1 ∈ S.toNonUnitalSubalgebra
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.toNonUnitalSubalgebra.toSubalgebra ⋯ = S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : NonUnitalSubalgebra R A<VAR>h1 : 1 ∈ S<GOAL>(S.toSubalgebra h1).toNonUnitalSubalgebra = S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : NonUnitalSubalgebra R A<GOAL>Subalgebra.toSubmodule (Algebra.adjoin R ↑s) = Submodule.span R {1} ⊔ s.toSubmodule
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>NonUnitalAlgebra.adjoin R s ≤ (Algebra.adjoin R s).toNonUnitalSubalgebra
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Algebra.adjoin R ↑(NonUnitalAlgebra.adjoin R s) = Algebra.adjoin R s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>Semiring C<VAR>Algebra R C<VAR>f : A →ₙₐ[R] C<VAR>S : Subalgebra R C<GOAL>(Unitization.lift f).range ≤ S ↔ NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>Semiring C<VAR>Algebra R C<VAR>f : A →ₙₐ[R] C<GOAL>(Unitization.lift f).range = Algebra.adjoin R ↑(NonUnitalAlgHom.range f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>x : Unitization R ↥s<GOAL>(NonUnitalSubalgebra.unitization s) x = (algebraMap R A) x.fst + ↑x.snd
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<GOAL>(NonUnitalSubalgebra.unitization s).range = Algebra.adjoin R ↑s
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s<VAR>FunLike F (Unitization R ↥s) A<VAR>AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<GOAL>Function.Injective ⇑f
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>A : Type u_4<VAR>Field R<VAR>Ring A<VAR>Algebra R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h1 : 1 ∉ s<VAR>FunLike F (Unitization R ↥s) A<VAR>AlgHomClass F R (Unitization R ↥s) A<VAR>f : F<VAR>hf : ∀ (x : ↥s), f ↑x = ↑x<GOAL>Function.Injective ⇑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Field R<VAR>Ring A<VAR>Algebra R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h1 : 1 ∉ s<GOAL>Function.Injective ⇑(NonUnitalSubalgebra.unitization s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Field R<VAR>Ring A<VAR>Algebra R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<VAR>h1 : 1 ∉ s<VAR>a : Unitization R ↥s<GOAL>↑((NonUnitalSubalgebra.unitizationAlgEquiv s h1) a) = (algebraMap R A) a.fst + ↑a.snd
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>1 ∈ S.toNonUnitalSubsemiring
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>S.toNonUnitalSubsemiring.toSubsemiring ⋯ = S
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>S : NonUnitalSubsemiring R<VAR>h1 : 1 ∈ S<GOAL>(S.toSubsemiring h1).toNonUnitalSubsemiring = S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>SetLike S R<VAR>hSR : NonUnitalSubsemiringClass S R<VAR>s : S<VAR>x : Unitization ℕ ↥s<GOAL>(NonUnitalSubsemiring.unitization s) x = ↑x.fst + ↑x.snd
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>SetLike S R<VAR>hSR : NonUnitalSubsemiringClass S R<VAR>s : S<GOAL>(NonUnitalSubsemiring.unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Subring R<GOAL>1 ∈ S.toNonUnitalSubring
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Subring R<GOAL>S.toNonUnitalSubring.toSubring ⋯ = S
<VAR>R : Type u_1<VAR>Ring R<VAR>S : NonUnitalSubring R<VAR>h1 : 1 ∈ S<GOAL>(S.toSubring h1).toNonUnitalSubring = S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>SetLike S R<VAR>hSR : NonUnitalSubringClass S R<VAR>s : S<VAR>x : Unitization ℤ ↥s<GOAL>(NonUnitalSubring.unitization s) x = ↑x.fst + ↑x.snd
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>SetLike S R<VAR>hSR : NonUnitalSubringClass S R<VAR>s : S<GOAL>(NonUnitalSubring.unitization s).range = subalgebraOfSubring (Subring.closure ↑s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>1 ∈ S.toNonUnitalStarSubalgebra
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<GOAL>S.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ = S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>S : NonUnitalStarSubalgebra R A<VAR>h1 : 1 ∈ S<GOAL>(S.toStarSubalgebra h1).toNonUnitalStarSubalgebra = S
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>s : NonUnitalStarSubalgebra R A<GOAL>Subalgebra.toSubmodule (StarAlgebra.adjoin R ↑s).toSubalgebra = Submodule.span R {1} ⊔ s.toSubmodule
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>s : Set A<GOAL>NonUnitalStarAlgebra.adjoin R s ≤ (StarAlgebra.adjoin R s).toNonUnitalStarSubalgebra
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>s : Set A<GOAL>StarAlgebra.adjoin R ↑(NonUnitalStarAlgebra.adjoin R s) = StarAlgebra.adjoin R s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing R<VAR>StarRing A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>StarModule R A<VAR>Semiring C<VAR>StarRing C<VAR>Algebra R C<VAR>StarModule R C<VAR>f : A →⋆ₙₐ[R] C<VAR>S : StarSubalgebra R C<GOAL>(Unitization.starLift f).range ≤ S ↔ NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>StarRing R<VAR>StarRing A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>StarModule R A<VAR>Semiring C<VAR>StarRing C<VAR>Algebra R C<VAR>StarModule R C<VAR>f : A →⋆ₙₐ[R] C<GOAL>(Unitization.starLift f).range = StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>StarMemClass S A<VAR>s : S<VAR>x : Unitization R ↥s<GOAL>(NonUnitalStarSubalgebra.unitization s) x = (algebraMap R A) x.fst + ↑x.snd
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>StarMemClass S A<VAR>s : S<GOAL>(NonUnitalStarSubalgebra.unitization s).range = StarAlgebra.adjoin R ↑s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Field R<VAR>StarRing R<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>StarMemClass S A<VAR>s : S<VAR>h1 : 1 ∉ s<GOAL>Function.Injective ⇑(NonUnitalStarSubalgebra.unitization s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>Field R<VAR>StarRing R<VAR>Ring A<VAR>StarRing A<VAR>Algebra R A<VAR>StarModule R A<VAR>SetLike S A<VAR>hSA : NonUnitalSubringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>StarMemClass S A<VAR>s : S<VAR>h1 : 1 ∉ s<VAR>a : Unitization R ↥s<GOAL>↑((NonUnitalStarSubalgebra.unitizationStarAlgEquiv s h1) a) = (algebraMap R A) a.fst + ↑a.snd
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>Mul R<VAR>One R<VAR>Neg R<GOAL>isSemireal R ↔ 0 ≠ 1 ∧ ¬isSumSq (-1)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>Mul R<VAR>One R<VAR>Neg R<VAR>self : isSemireal R<GOAL>0 ≠ 1
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>Mul R<VAR>One R<VAR>Neg R<VAR>self : isSemireal R<GOAL>¬isSumSq (-1)
<VAR>R : Type u_2<VAR>Semiring R<VAR>f : RingAut R<VAR>r : R<GOAL>f • r = f r
<VAR>G : Type u_1<VAR>R : Type u_2<VAR>Group G<VAR>Semiring R<VAR>MulSemiringAction G R<VAR>x : G<GOAL>(MulSemiringAction.toRingAut G R) x = MulSemiringAction.toRingEquiv G R x
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>S.op.toSubmonoid = S.op
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>↑S.op = MulOpposite.unop ⁻¹' ↑S
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>x : Rᵐᵒᵖ<VAR>S : Subsemiring R<GOAL>x ∈ S.op ↔ MulOpposite.unop x ∈ S
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring Rᵐᵒᵖ<GOAL>S.unop.toSubmonoid = S.unop
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring Rᵐᵒᵖ<GOAL>↑S.unop = MulOpposite.op ⁻¹' ↑S
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>x : R<VAR>S : Subsemiring Rᵐᵒᵖ<GOAL>x ∈ S.unop ↔ MulOpposite.op x ∈ S
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>S.op.unop = S
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring Rᵐᵒᵖ<GOAL>S.unop.op = S
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S₁ : Subsemiring R<VAR>S₂ : Subsemiring Rᵐᵒᵖ<GOAL>S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S₁ : Subsemiring Rᵐᵒᵖ<VAR>S₂ : Subsemiring R<GOAL>S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S₁ S₂ : Subsemiring R<GOAL>S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S₁ S₂ : Subsemiring Rᵐᵒᵖ<GOAL>S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring Rᵐᵒᵖ<GOAL>(RelIso.symm Subsemiring.opEquiv) S = S.unop
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>Subsemiring.opEquiv S = S.op
<VAR>R : Type u_2<VAR>NonAssocSemiring R<GOAL>⊥.op = ⊥
<VAR>R : Type u_2<VAR>NonAssocSemiring R<GOAL>⊥.unop = ⊥
<VAR>R : Type u_2<VAR>NonAssocSemiring R<GOAL>⊤.op = ⊤
<VAR>R : Type u_2<VAR>NonAssocSemiring R<GOAL>⊤.unop = ⊤
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S₁ S₂ : Subsemiring R<GOAL>(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S₁ S₂ : Subsemiring Rᵐᵒᵖ<GOAL>(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop