ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Set (Subsemiring R)<GOAL>(sSup S).op = sSup (Subsemiring.unop ⁻¹' S)
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Set (Subsemiring Rᵐᵒᵖ)<GOAL>(sSup S).unop = sSup (Subsemiring.op ⁻¹' S)
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Set (Subsemiring R)<GOAL>(sInf S).op = sInf (Subsemiring.unop ⁻¹' S)
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Set (Subsemiring Rᵐᵒᵖ)<GOAL>(sInf S).unop = sInf (Subsemiring.op ⁻¹' S)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : ι → Subsemiring R<GOAL>(iSup S).op = ⨆ i, (S i).op
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : ι → Subsemiring Rᵐᵒᵖ<GOAL>(iSup S).unop = ⨆ i, (S i).unop
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : ι → Subsemiring R<GOAL>(iInf S).op = ⨅ i, (S i).op
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : ι → Subsemiring Rᵐᵒᵖ<GOAL>(iInf S).unop = ⨅ i, (S i).unop
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>s : Set R<GOAL>(Subsemiring.closure s).op = Subsemiring.closure (MulOpposite.unop ⁻¹' s)
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>s : Set Rᵐᵒᵖ<GOAL>(Subsemiring.closure s).unop = Subsemiring.closure (MulOpposite.op ⁻¹' s)
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<VAR>b : { b // (fun x => x ∈ S.op) b }<GOAL>↑(S.addEquivOp.symm b) = MulOpposite.unop ↑b
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<VAR>a : { a // (fun x => x ∈ S.toSubmonoid) a }<GOAL>↑(S.addEquivOp a) = MulOpposite.op ↑a
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>∀ (a : (↥S.op)ᵐᵒᵖ), ↑(S.ringEquivOpMop.symm a) = MulOpposite.unop ↑(MulOpposite.unop a)
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>∀ (a : ↥S), S.ringEquivOpMop a = MulOpposite.op (S.addEquivOp a)
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>∀ (a : (↥S)ᵐᵒᵖ), ↑(S.mopRingEquivOp a) = MulOpposite.op ↑(MulOpposite.unop a)
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<GOAL>∀ (a : ↥S.op), S.mopRingEquivOp.symm a = MulOpposite.op (S.addEquivOp.symm a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>x y : Unitization R A<VAR>h1 : x.fst = y.fst<VAR>h2 : x.snd = y.snd<GOAL>x = y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Zero A<VAR>r : R<GOAL>(Unitization.inl r).fst = r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Zero A<VAR>r : R<GOAL>(Unitization.inl r).snd = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Zero R<VAR>a : A<GOAL>(↑a).fst = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Zero R<VAR>a : A<GOAL>(↑a).snd = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Zero A<GOAL>Function.Injective Unitization.inl
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Zero R<GOAL>Function.Injective Unitization.inr
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Zero R<VAR>Zero A<GOAL>Unitization.fst 0 = 0
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Zero R<VAR>Zero A<GOAL>Unitization.snd 0 = 0
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Add R<VAR>Add A<VAR>x₁ x₂ : Unitization R A<GOAL>(x₁ + x₂).fst = x₁.fst + x₂.fst
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Add R<VAR>Add A<VAR>x₁ x₂ : Unitization R A<GOAL>(x₁ + x₂).snd = x₁.snd + x₂.snd
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Neg R<VAR>Neg A<VAR>x : Unitization R A<GOAL>(-x).fst = -x.fst
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Neg R<VAR>Neg A<VAR>x : Unitization R A<GOAL>(-x).snd = -x.snd
<VAR>S : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>SMul S R<VAR>SMul S A<VAR>s : S<VAR>x : Unitization R A<GOAL>(s • x).fst = s • x.fst
<VAR>S : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>SMul S R<VAR>SMul S A<VAR>s : S<VAR>x : Unitization R A<GOAL>(s • x).snd = s • x.snd
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Zero R<VAR>Zero A<GOAL>Unitization.inl 0 = 0
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Add R<VAR>AddZeroClass A<VAR>r₁ r₂ : R<GOAL>Unitization.inl (r₁ + r₂) = Unitization.inl r₁ + Unitization.inl r₂
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Neg R<VAR>AddGroup A<VAR>r : R<GOAL>Unitization.inl (-r) = -Unitization.inl r
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>AddGroup R<VAR>AddGroup A<VAR>r₁ r₂ : R<GOAL>Unitization.inl (r₁ - r₂) = Unitization.inl r₁ - Unitization.inl r₂
<VAR>S : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Monoid S<VAR>AddMonoid A<VAR>SMul S R<VAR>DistribMulAction S A<VAR>s : S<VAR>r : R<GOAL>Unitization.inl (s • r) = s • Unitization.inl r
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Zero R<VAR>Zero A<GOAL>↑0 = 0
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>AddZeroClass R<VAR>Add A<VAR>m₁ m₂ : A<GOAL>↑(m₁ + m₂) = ↑m₁ + ↑m₂
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>AddGroup R<VAR>Neg A<VAR>m : A<GOAL>↑(-m) = -↑m
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>AddGroup R<VAR>AddGroup A<VAR>m₁ m₂ : A<GOAL>↑(m₁ - m₂) = ↑m₁ - ↑m₂
<VAR>S : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Zero R<VAR>Zero S<VAR>SMulWithZero S R<VAR>SMul S A<VAR>r : S<VAR>m : A<GOAL>↑(r • m) = r • ↑m
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>AddZeroClass R<VAR>AddZeroClass A<VAR>x : Unitization R A<GOAL>Unitization.inl x.fst + ↑x.snd = x
<VAR>R : Type u_5<VAR>A : Type u_6<VAR>AddZeroClass R<VAR>AddZeroClass A<VAR>P : Unitization R A → Prop<VAR>inl_add_inr : ∀ (r : R) (a : A), P (Unitization.inl r + ↑a)<VAR>x : Unitization R A<GOAL>P x
<VAR>S : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>N : Type u_5<VAR>Semiring S<VAR>AddCommMonoid R<VAR>AddCommMonoid A<VAR>AddCommMonoid N<VAR>Module S R<VAR>Module S A<VAR>Module S N<VAR>f g : Unitization R A →ₗ[S] N<VAR>hl : ∀ (r : R), f (Unitization.inl r) = g (Unitization.inl r)<VAR>hr : ∀ (a : A), f ↑a = g ↑a<GOAL>f = g
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>a : A<GOAL>(Unitization.inrHom R A) a = ↑a
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>x : Unitization R A<GOAL>(Unitization.sndHom R A) x = x.snd
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>One R<VAR>Zero A<GOAL>Unitization.fst 1 = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>One R<VAR>Zero A<GOAL>Unitization.snd 1 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Mul R<VAR>Add A<VAR>Mul A<VAR>SMul R A<VAR>x₁ x₂ : Unitization R A<GOAL>(x₁ * x₂).fst = x₁.fst * x₂.fst
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Mul R<VAR>Add A<VAR>Mul A<VAR>SMul R A<VAR>x₁ x₂ : Unitization R A<GOAL>(x₁ * x₂).snd = x₁.fst • x₂.snd + x₂.fst • x₁.snd + x₁.snd * x₂.snd
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>One R<VAR>Zero A<GOAL>Unitization.inl 1 = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>r₁ r₂ : R<GOAL>Unitization.inl (r₁ * r₂) = Unitization.inl r₁ * Unitization.inl r₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>r₁ r₂ : R<GOAL>Unitization.inl r₁ * Unitization.inl r₂ = Unitization.inl (r₁ * r₂)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Mul A<VAR>SMulWithZero R A<VAR>a₁ a₂ : A<GOAL>↑(a₁ * a₂) = ↑a₁ * ↑a₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>r : R<VAR>a : A<GOAL>Unitization.inl r * ↑a = ↑(r • a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>r : R<VAR>a : A<GOAL>↑a * Unitization.inl r = ↑(r • a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>r : R<GOAL>(Unitization.inlRingHom R A) r = Unitization.inl r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Star R<VAR>Star A<VAR>x : Unitization R A<GOAL>(star x).fst = star x.fst
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Star R<VAR>Star A<VAR>x : Unitization R A<GOAL>(star x).snd = star x.snd
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Star R<VAR>AddMonoid A<VAR>StarAddMonoid A<VAR>r : R<GOAL>Unitization.inl (star r) = star (Unitization.inl r)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>AddMonoid R<VAR>StarAddMonoid R<VAR>Star A<VAR>a : A<GOAL>↑(star a) = star ↑a
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>Algebra S R<VAR>DistribMulAction S A<VAR>IsScalarTower S R A<GOAL>⇑(algebraMap S (Unitization R A)) = Unitization.inl ∘ ⇑(algebraMap S R)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>Algebra S R<VAR>DistribMulAction S A<VAR>IsScalarTower S R A<GOAL>algebraMap S (Unitization R A) = (Unitization.inlRingHom R A).comp (algebraMap S R)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>⇑(algebraMap R (Unitization R A)) = Unitization.inl
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>algebraMap R (Unitization R A) = Unitization.inlRingHom R A
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : Unitization R A<GOAL>(Unitization.fstHom R A) x = x.fst
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>a : A<GOAL>(Unitization.inrNonUnitalAlgHom R A) a = ↑a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarAddMonoid R<VAR>NonUnitalSemiring A<VAR>Star A<VAR>Module R A<VAR>a : A<GOAL>(Unitization.inrNonUnitalStarAlgHom R A) a = ↑a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarAddMonoid R<VAR>NonUnitalSemiring A<VAR>Star A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>a : A<GOAL>↑((Unitization.inrRangeEquiv R A) a) = ↑(Unitization.inrNonUnitalStarAlgHom R A) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>StarAddMonoid R<VAR>NonUnitalSemiring A<VAR>Star A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<GOAL>∀ (a : ↥(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom R A))), (Unitization.inrRangeEquiv R A).symm a = (↑a).snd
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring S<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>B : Type u_4<VAR>Semiring B<VAR>Algebra S B<VAR>Algebra S R<VAR>DistribMulAction S A<VAR>IsScalarTower S R A<VAR>F : Type u_6<VAR>FunLike F (Unitization R A) B<VAR>AlgHomClass F S (Unitization R A) B<VAR>φ ψ : F<VAR>h : ∀ (a : A), φ ↑a = ψ ↑a<VAR>h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)<GOAL>φ = ψ
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>C : Type u_5<VAR>Semiring C<VAR>Algebra R C<VAR>F : Type u_6<VAR>FunLike F (Unitization R A) C<VAR>AlgHomClass F R (Unitization R A) C<VAR>φ ψ : F<VAR>h : ∀ (a : A), φ ↑a = ψ ↑a<GOAL>φ = ψ
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>C : Type u_5<VAR>Semiring C<VAR>Algebra R C<VAR>φ ψ : Unitization R A →ₐ[R] C<VAR>h : (↑φ).comp (Unitization.inrNonUnitalAlgHom R A) = (↑ψ).comp (Unitization.inrNonUnitalAlgHom R A)<GOAL>φ = ψ
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>C : Type u_5<VAR>Semiring C<VAR>Algebra R C<VAR>φ : A →ₙₐ[R] C<VAR>x : Unitization R A<GOAL>φ.toAlgHom x = (algebraMap R C) x.fst + φ x.snd
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>C : Type u_5<VAR>Semiring C<VAR>Algebra R C<VAR>φ : A →ₙₐ[R] C<GOAL>Unitization.lift φ = φ.toAlgHom
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>C : Type u_5<VAR>Semiring C<VAR>Algebra R C<VAR>φ : A →ₙₐ[R] C<VAR>x : Unitization R A<GOAL>(Unitization.lift φ) x = (algebraMap R C) x.fst + φ x.snd
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>C : Type u_5<VAR>Semiring C<VAR>Algebra R C<VAR>φ : Unitization R A →ₐ[R] C<GOAL>Unitization.lift.symm φ = (NonUnitalAlgHomClass.toNonUnitalAlgHom φ).comp (Unitization.inrNonUnitalAlgHom R A)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>C : Type u_5<VAR>Semiring C<VAR>Algebra R C<VAR>φ : Unitization R A →ₐ[R] C<VAR>a : A<GOAL>(Unitization.lift.symm φ) a = φ ↑a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<GOAL>⇑(NonUnitalAlgHom.toAlgHom 0) = Unitization.fst
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>Semiring C<VAR>Algebra R C<VAR>StarRing C<VAR>φ ψ : Unitization R A →⋆ₐ[R] C<VAR>h : (↑φ).comp (Unitization.inrNonUnitalStarAlgHom R A) = (↑ψ).comp (Unitization.inrNonUnitalStarAlgHom R A)<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>Semiring C<VAR>Algebra R C<VAR>StarRing C<VAR>StarModule R C<VAR>φ : Unitization R A →⋆ₐ[R] C<GOAL>Unitization.starLift.symm φ = φ.toNonUnitalStarAlgHom.comp (Unitization.inrNonUnitalStarAlgHom R A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>Semiring C<VAR>Algebra R C<VAR>StarRing C<VAR>StarModule R C<VAR>φ : A →⋆ₙₐ[R] C<VAR>x : Unitization R A<GOAL>(Unitization.starLift φ) x = (algebraMap R C) x.fst + φ x.snd
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>C : Type u_3<VAR>CommSemiring R<VAR>StarRing R<VAR>NonUnitalSemiring A<VAR>StarRing A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>Semiring C<VAR>Algebra R C<VAR>StarRing C<VAR>StarModule R C<VAR>φ : A →⋆ₙₐ[R] C<GOAL>Unitization.starLift φ = { toAlgHom := φ.toAlgHom, map_star' := ⋯ }
<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>φ : Unitization R A →ₐ[R] C<VAR>a : A<GOAL>(Unitization.lift.symm φ) a = φ ↑a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>AddCommMonoid A<VAR>Mul A<VAR>SMulWithZero R A<VAR>StarAddMonoid R<VAR>Star A<VAR>a : A<GOAL>IsStarNormal ↑a ↔ IsStarNormal a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarAddMonoid R<VAR>Star A<VAR>a : A<GOAL>IsSelfAdjoint ↑a ↔ IsSelfAdjoint a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>StarAddMonoid R<VAR>Star A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>IsSelfAdjoint ↑a
<VAR>R : Type u_1<VAR>self : PreQuasiregular R<GOAL>PreQuasiregular.equiv.symm self = self.val
<VAR>R : Type u_1<VAR>val : R<GOAL>(PreQuasiregular.equiv val).val = val
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<GOAL>PreQuasiregular.val 1 = 0
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>x y : PreQuasiregular R<GOAL>(x * y).val = y.val + x.val + x.val * y.val
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>u : (PreQuasiregular R)ˣ<GOAL>(↑u⁻¹).val + (↑u).val + (↑u).val * (↑u⁻¹).val = 0
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>u : (PreQuasiregular R)ˣ<GOAL>(↑u).val + (↑u⁻¹).val + (↑u⁻¹).val * (↑u).val = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : (Unitization R A)ˣ<GOAL>x ∈ Unitization.unitsFstOne R A ↔ (↑x).fst = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : ↥(Unitization.unitsFstOne R A)<GOAL>(↑↑x).fst = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : ↥(Unitization.unitsFstOne R A)<GOAL>(↑(↑x)⁻¹).fst = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : ↥(Unitization.unitsFstOne R A)<GOAL>↑((Unitization.unitsFstOne_mulEquiv_quasiregular R) x) = PreQuasiregular.equiv (↑↑x).snd
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : (PreQuasiregular A)ˣ<GOAL>↑(↑((Unitization.unitsFstOne_mulEquiv_quasiregular R).symm x))⁻¹ = 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : (PreQuasiregular A)ˣ<GOAL>↑↑((Unitization.unitsFstOne_mulEquiv_quasiregular R).symm x) = 1 + ↑(PreQuasiregular.equiv.symm ↑x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : ↥(Unitization.unitsFstOne R A)<GOAL>↑((Unitization.unitsFstOne_mulEquiv_quasiregular R) x)⁻¹ = PreQuasiregular.equiv (↑↑x⁻¹).snd
<VAR>R : Type u_1<VAR>NonUnitalSemiring R<VAR>x : R<GOAL>IsQuasiregular x ↔ ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>NonUnitalSemiring R<VAR>NonUnitalSemiring S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>x : R<VAR>hx : IsQuasiregular x<GOAL>IsQuasiregular (f x)
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : R<VAR>hx : IsQuasiregular x<GOAL>IsUnit (1 + x)
<VAR>R : Type u_1<VAR>Ring R<VAR>x : R<GOAL>IsQuasiregular x ↔ IsUnit (1 + x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>x : A<GOAL>IsQuasiregular x ↔ IsUnit (1 + ↑x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalRing A<VAR>Module R A<VAR>a : A<VAR>r : R<VAR>hr : ¬IsUnit r<GOAL>r ∈ quasispectrum R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalRing A<VAR>Module R A<VAR>Nontrivial R<VAR>a : A<GOAL>0 ∈ quasispectrum R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalRing A<VAR>Module R A<VAR>Nontrivial R<VAR>a : A<GOAL>↑0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalRing A<VAR>Module R A<VAR>a : A<VAR>r : Rˣ<VAR>hr : ¬IsQuasiregular (-(r⁻¹ • a))<GOAL>↑r ∈ quasispectrum R a
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<GOAL>quasispectrum R a = spectrum R a ∪ {r | ¬IsUnit r}
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<GOAL>spectrum R a ⊆ quasispectrum R a
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Semifield R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<GOAL>quasispectrum R a = spectrum R a ∪ {0}
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>Semifield R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>x : R<GOAL>x ∈ quasispectrum R a ↔ x = 0 ∨ x ∈ spectrum R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>a : A<GOAL>IsQuasiregular ↑a ↔ IsQuasiregular a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>CommSemiring R<VAR>CommRing S<VAR>Nontrivial S<VAR>NonUnitalRing A<VAR>Algebra R S<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>a : A<GOAL>0 ∈ spectrum R ↑a
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommRing R<VAR>NonUnitalRing A<VAR>Module R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>a : A<VAR>r : R<VAR>hr : ¬IsUnit r<GOAL>r ∈ spectrum R ↑a
<VAR>R : Type u_3<VAR>A : Type u_4<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<GOAL>quasispectrum R a = spectrum R ↑a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Algebra R S<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>a : A<GOAL>quasispectrum R a = spectrum R ↑a
<VAR>𝕜 : Type u_3<VAR>A : Type u_4<VAR>OrderedCommSemiring 𝕜<VAR>NonUnitalRing A<VAR>PartialOrder A<VAR>Module 𝕜 A<VAR>self : NonnegSpectrumClass 𝕜 A<VAR>a : A<GOAL>0 ≤ a → ∀ x ∈ quasispectrum 𝕜 a, 0 ≤ x
<VAR>𝕜 : Type u_3<VAR>A : Type u_4<VAR>LinearOrderedSemifield 𝕜<VAR>Ring A<VAR>PartialOrder A<VAR>Algebra 𝕜 A<GOAL>NonnegSpectrumClass 𝕜 A ↔ ∀ (a : A), 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x
<VAR>𝕜 : Type u_3<VAR>A : Type u_4<VAR>OrderedCommSemiring 𝕜<VAR>Ring A<VAR>PartialOrder A<VAR>Algebra 𝕜 A<VAR>NonnegSpectrumClass 𝕜 A<VAR>a : A<VAR>ha : 0 ≤ a<VAR>x : 𝕜<VAR>hx : x ∈ spectrum 𝕜 a<GOAL>0 ≤ x
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>Algebra R S<VAR>a : A<VAR>f : S → R<VAR>self : QuasispectrumRestricts a f<GOAL>Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>Algebra R S<VAR>a : A<VAR>f : S → R<VAR>self : QuasispectrumRestricts a f<GOAL>Function.LeftInverse f ⇑(algebraMap R S)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>Algebra R S<VAR>a : A<VAR>f : S → R<GOAL>QuasispectrumRestricts a f ↔ Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a) ∧ Function.LeftInverse f ⇑(algebraMap R S)
<VAR>S : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Algebra R S<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>a : A<VAR>r : R<GOAL>(algebraMap R S) r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a
<VAR>S : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Algebra R S<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>a : A<GOAL>⇑(algebraMap R S) ⁻¹' quasispectrum S a = quasispectrum R a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>Algebra R S<VAR>a : A<VAR>f : S → R<VAR>h : QuasispectrumRestricts a f<GOAL>f 0 = 0
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>Algebra R S<VAR>a : A<VAR>f : S → R<VAR>hf : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h : quasispectrum S a ⊆ Set.range ⇑(algebraMap R S)<GOAL>QuasispectrumRestricts a f
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Algebra R S<VAR>a : A<VAR>f : S → R<VAR>IsScalarTower R S A<VAR>h : QuasispectrumRestricts a f<GOAL>⇑(algebraMap R S) '' quasispectrum R a = quasispectrum S a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Algebra R S<VAR>a : A<VAR>f : S → R<VAR>IsScalarTower R S A<VAR>h : QuasispectrumRestricts a f<GOAL>f '' quasispectrum S a = quasispectrum R a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>Semifield R<VAR>Field S<VAR>NonUnitalRing A<VAR>Module R A<VAR>Module S A<VAR>IsScalarTower S A A<VAR>SMulCommClass S A A<VAR>Algebra R S<VAR>a : A<VAR>f : S → R<VAR>IsScalarTower R S A<VAR>h : QuasispectrumRestricts a f<VAR>s : S<VAR>hs : s ∈ quasispectrum S a<GOAL>f s ∈ quasispectrum R a