ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>h : algebraMap R A = (algebraMap S A).comp (algebraMap R S)<GOAL>IsScalarTower R S A
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>IsScalarTower R S A<GOAL>algebraMap R A = (algebraMap S A).comp (algebraMap R S)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>x : R<GOAL>(algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
<VAR>S : Type u<VAR>A : Type v<VAR>CommSemiring S<VAR>Semiring A<VAR>h1 h2 : Algebra S A<VAR>h : ∀ (r : S) (x : A), (let_fun I := h1; r • x) = r • x<GOAL>h1 = h2
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>y : S<GOAL>(IsScalarTower.toAlgHom R S A) y = (algebraMap S A) y
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>IsScalarTower R S A<GOAL>↑(IsScalarTower.toAlgHom R S A) = algebraMap S A
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>IsScalarTower R S A<GOAL>⇑(IsScalarTower.toAlgHom R S A) = ⇑(algebraMap S A)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>r : R<GOAL>f ((algebraMap R A) r) = (algebraMap R B) r
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(↑f).comp (algebraMap R A) = algebraMap R B
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x : A<GOAL>(AlgHom.restrictScalars R f) x = f x
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>↑(AlgHom.restrictScalars R f) = ↑f
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>⇑(AlgHom.restrictScalars R f) = ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<GOAL>Function.Injective (AlgHom.restrictScalars R)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A ≃ₐ[S] B<VAR>x : A<GOAL>(AlgEquiv.restrictScalars R f) x = f x
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A ≃ₐ[S] B<GOAL>↑(AlgEquiv.restrictScalars R f) = ↑f
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A ≃ₐ[S] B<GOAL>⇑(AlgEquiv.restrictScalars R f) = ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<GOAL>Function.Injective (AlgEquiv.restrictScalars R)
<VAR>R : Type u<VAR>A : Type w<VAR>M : Type v₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>hsur : Function.Surjective ⇑(algebraMap R A)<VAR>X : Set M<GOAL>Submodule.restrictScalars R (Submodule.span A X) = Submodule.span R X
<VAR>R : Type u<VAR>A : Type w<VAR>M : Type v₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>h : Function.Surjective ⇑(algebraMap R A)<VAR>s : Set M<GOAL>↑(Submodule.span A s) = ↑(Submodule.span R s)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>s : Set S<VAR>t : Set A<VAR>k : S<VAR>hks : k ∈ Submodule.span R s<VAR>x : A<VAR>hx : x ∈ t<GOAL>k • x ∈ Submodule.span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>s : Set S<VAR>hs : Submodule.span R s = ⊤<VAR>t : Set A<GOAL>Submodule.span R (s • t) = Submodule.restrictScalars R (Submodule.span S t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>s : Set S<VAR>hs : Submodule.span R s = ⊤<VAR>t : Set A<VAR>k : S<VAR>x : A<VAR>hx : x ∈ Submodule.span R (s • t)<GOAL>k • x ∈ Submodule.span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>s : Set S<VAR>hs : Submodule.span R s = ⊤<VAR>t : Set A<VAR>k : S<VAR>x : A<VAR>hx : x ∈ Submodule.span R t<GOAL>k • x ∈ Submodule.span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>a : Set R<GOAL>Submodule.span R (⇑(algebraMap R S) '' a) = Submodule.map (Algebra.linearMap R S) (Submodule.span R a)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>T : Type u_2<VAR>CommSemiring S<VAR>Semiring T<VAR>Module R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>a : Set S<GOAL>Submodule.span R (⇑(algebraMap S T) '' a) = Submodule.map (↑R (Algebra.linearMap S T)) (Submodule.span R a)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>T : Type u_2<VAR>CommSemiring S<VAR>Semiring T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>x : S<VAR>a : Set S<VAR>hx : x ∈ Submodule.span R a<GOAL>(algebraMap S T) x ∈ Submodule.span R (⇑(algebraMap S T) '' a)
<VAR>R : Type u<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>AddCommGroup M<VAR>Module R M<VAR>Module A M<VAR>Module B M<VAR>IsScalarTower R A M<VAR>IsScalarTower R B M<VAR>SMulCommClass A B M<VAR>NoZeroSMulDivisors A M<VAR>x : A<VAR>hx : x ≠ 0<GOAL>Function.Injective ⇑((Algebra.lsmul R B M) x)
<VAR>R : Type u_1<VAR>Distrib R<VAR>r : R<GOAL>⇑(AddHom.mulLeft r) = fun x => r * x
<VAR>R : Type u_1<VAR>Distrib R<VAR>r : R<GOAL>⇑(AddHom.mulRight r) = fun a => a * r
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<VAR>r : R<GOAL>⇑(AddMonoidHom.mulLeft r) = HMul.hMul r
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<VAR>r : R<GOAL>⇑(AddMonoidHom.mulRight r) = fun x => x * r
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<VAR>a r : R<GOAL>(AddMonoidHom.mulRight r) a = a * r
<VAR>α : Type u_2<VAR>Group α<VAR>HasDistribNeg α<VAR>a : α<GOAL>(-a)⁻¹ = -a⁻¹
<VAR>α : Type u_2<VAR>NonUnitalCommRing α<VAR>b c x : α<VAR>h : x * x - b * x + c = 0<GOAL>∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
<VAR>α : Type u_2<VAR>NonAssocRing α<VAR>Nontrivial α<VAR>a : α<GOAL>a + 1 ≠ a
<VAR>α : Type u_2<VAR>NonAssocRing α<VAR>Nontrivial α<VAR>a : α<GOAL>a - 1 ≠ a
<VAR>α : Type u_2<VAR>NonUnitalNonAssocRing α<VAR>IsLeftCancelMulZero α<GOAL>NoZeroDivisors α
<VAR>α : Type u_2<VAR>NonUnitalNonAssocRing α<VAR>IsRightCancelMulZero α<GOAL>NoZeroDivisors α
<VAR>α : Type u_2<VAR>NonUnitalNonAssocRing α<GOAL>IsCancelMulZero α ↔ NoZeroDivisors α
<VAR>α : Type u_2<VAR>Ring α<VAR>h : Nontrivial α<VAR>NoZeroDivisors α<GOAL>IsDomain α
<VAR>α : Type u_2<VAR>Semiring α<GOAL>IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α
<VAR>α : Type u_2<VAR>Semiring α<GOAL>IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α
<VAR>α : Type u_2<VAR>Ring α<GOAL>IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α
<VAR>α : Type u_2<VAR>Ring α<GOAL>NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>K : ι → Subalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<GOAL>↑(iSup K) = ⋃ i, ↑(K i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>K : ι → Subalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)<VAR>T : Subalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥(K i)<VAR>h : K i ≤ T<GOAL>(Subalgebra.iSupLift K dir f hf T hT) ((Subalgebra.inclusion h) x) = (f i) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>K : ι → Subalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)<VAR>T : Subalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>h : K i ≤ T<GOAL>(Subalgebra.iSupLift K dir f hf T hT).comp (Subalgebra.inclusion h) = f i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>K : ι → Subalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)<VAR>T : Subalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥(K i)<VAR>hx : ↑x ∈ T<GOAL>(Subalgebra.iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>ι : Type u_4<VAR>Nonempty ι<VAR>K : ι → Subalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)<VAR>T : Subalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥T<VAR>hx : ↑x ∈ K i<GOAL>(Subalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩
<VAR>R : Type u_1<VAR>LinearOrderedSemiring R<VAR>u : Rˣ<GOAL>u ∈ Units.posSubgroup R ↔ 0 < ↑u
<VAR>R : Type u<VAR>CommSemiring R<VAR>r : R<GOAL>(algebraMap R PUnit.{u_2 + 1}) r = PUnit.unit
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R (ULift.{u_2, w} A)) r = { down := (algebraMap R A) r }
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>((algebraMap R (ULift.{u_2, w} A)) r).down = (algebraMap R A) r
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Subsemiring R<GOAL>algebraMap (↥S) R = S.subtype
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Subsemiring R<GOAL>⇑(algebraMap (↥S) R) = Subtype.val
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Subsemiring R<VAR>x : ↥S<GOAL>(algebraMap (↥S) R) x = ↑x
<VAR>R : Type u_2<VAR>CommRing R<VAR>S : Subring R<GOAL>algebraMap (↥S) R = S.subtype
<VAR>R : Type u_2<VAR>CommRing R<VAR>S : Subring R<GOAL>⇑(algebraMap (↥S) R) = Subtype.val
<VAR>R : Type u_2<VAR>CommRing R<VAR>S : Subring R<VAR>x : ↥S<GOAL>(algebraMap (↥S) R) x = ↑x
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submonoid R<VAR>x : ↥M<GOAL>(algebraMap R S) ↑x ∈ Algebra.algebraMapSubmonoid S M
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>x : A<VAR>r : R<GOAL>x * (x - (algebraMap R A) r) = (x - (algebraMap R A) r) * x
<VAR>R : Type u<VAR>A : Type w<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>x : A<VAR>r : R<VAR>n : ℕ<GOAL>x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>CommSemiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass S R M<VAR>SMul R S<VAR>IsScalarTower R S M<VAR>a : R<GOAL>(algebraMap R (Module.End S M)) a = a • LinearMap.id
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>CommSemiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass S R M<VAR>SMul R S<VAR>IsScalarTower R S M<VAR>a : R<VAR>m : M<GOAL>((algebraMap R (Module.End S M)) a) m = a • m
<VAR>K : Type u<VAR>V : Type v<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>a : K<VAR>ha : a ≠ 0<GOAL>LinearMap.ker ((algebraMap K (Module.End K V)) a) = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>CommSemiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass S R M<VAR>SMul R S<VAR>IsScalarTower R S M<VAR>x : R<VAR>h : IsUnit ((algebraMap R (Module.End S M)) x)<VAR>m m' : M<GOAL>↑h.unit⁻¹ m = m' ↔ m = x • m'
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>CommSemiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>SMulCommClass S R M<VAR>SMul R S<VAR>IsScalarTower R S M<VAR>x : R<VAR>h : IsUnit ((algebraMap R (Module.End S M)) x)<VAR>m m' : M<GOAL>m' = ↑h.unit⁻¹ m ↔ m = x • m'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₗ[R] B<VAR>a : A<VAR>r : R<GOAL>f ((algebraMap R A) r * a) = (algebraMap R B) r * f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₗ[R] B<VAR>a : A<VAR>r : R<GOAL>f (a * (algebraMap R A) r) = f a * (algebraMap R B) r
<VAR>R : Type u_1<VAR>Ring R<GOAL>algebraMap ℤ R = Int.castRingHom R
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>NoZeroDivisors A<VAR>h : Function.Injective ⇑(algebraMap R A)<GOAL>NoZeroSMulDivisors R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>Nontrivial A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<GOAL>Function.Injective ⇑(algebraMap R A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>n : ℕ<VAR>CommRing R<VAR>NeZero ↑n<VAR>Ring A<VAR>Nontrivial A<VAR>Algebra R A<VAR>NoZeroSMulDivisors R A<GOAL>NeZero ↑n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>Ring A<VAR>IsDomain A<VAR>Algebra R A<GOAL>NoZeroSMulDivisors R A ↔ Function.Injective ⇑(algebraMap R A)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>r : R<VAR>m : M<GOAL>r • m = (algebraMap R A) r • m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>r : R<VAR>m : M<GOAL>(algebraMap R A) r • m = r • m
<VAR>R : Type u_5<VAR>A : Type u_6<VAR>M : Type u_7<VAR>CommRing R<VAR>Ring A<VAR>IsDomain A<VAR>Algebra R A<VAR>AddCommGroup M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>NoZeroSMulDivisors R A<VAR>NoZeroSMulDivisors A M<GOAL>NoZeroSMulDivisors R M
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>r : R<VAR>a : A<VAR>m : M<GOAL>a • r • m = r • a • m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>Semiring R<VAR>Semiring S<VAR>SMul R S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[S] N<GOAL>LinearMap.ker (↑R f) = Submodule.restrictScalars R (LinearMap.ker f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₗ[R] B<VAR>hf : f 1 = 1<VAR>r : R<VAR>h : IsUnit ((algebraMap R A) r)<GOAL>IsUnit ((algebraMap R B) r)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommSemiring F<VAR>Semiring E<VAR>Algebra F E<VAR>b : F →ₗ[F] E<VAR>hb : Function.Injective ⇑b<GOAL>Function.Injective ⇑(algebraMap F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommSemiring F<VAR>Semiring E<VAR>Algebra F E<VAR>b : F →ₗ[F] E<VAR>hb : Function.Surjective ⇑b<GOAL>Function.Surjective ⇑(algebraMap F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommSemiring F<VAR>Semiring E<VAR>Algebra F E<VAR>b : F →ₗ[F] E<VAR>hb : Function.Bijective ⇑b<GOAL>Function.Bijective ⇑(algebraMap F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommSemiring F<VAR>Semiring E<VAR>Algebra F E<VAR>b : F ≃ₗ[F] E<GOAL>Function.Bijective ⇑(algebraMap F E)
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>h : Function.Surjective ⇑(algebraMap R S)<VAR>l : M →ₗ[R] N<VAR>x : M<GOAL>(LinearMap.extendScalarsOfSurjective h l) x = l x
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>h : Function.Surjective ⇑(algebraMap R S)<VAR>f : M ≃ₗ[R] N<VAR>x : M<GOAL>(LinearEquiv.extendScalarsOfSurjective h f) x = f x
<VAR>R : Type u_1<VAR>S : Type u_4<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>h : Function.Surjective ⇑(algebraMap R S)<VAR>f : M ≃ₗ[R] N<GOAL>(LinearEquiv.extendScalarsOfSurjective h f).symm = LinearEquiv.extendScalarsOfSurjective h f.symm
<VAR>R : Fin 2 → Type u_1<VAR>(i : Fin 2) → Semiring (R i)<GOAL>∀ (a : R 0 × R 1) (i : Fin 2), (RingEquiv.piFinTwo R).symm a i = (piFinTwoEquiv R).invFun a i
<VAR>R : Fin 2 → Type u_1<VAR>(i : Fin 2) → Semiring (R i)<VAR>a : (i : Fin 2) → R i<GOAL>(RingEquiv.piFinTwo R) a = (piFinTwoEquiv R) a
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring R<GOAL>S.op.toSubsemiring = S.op
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring R<GOAL>↑S.op = MulOpposite.unop ⁻¹' ↑S
<VAR>R : Type u_2<VAR>Ring R<VAR>x : Rᵐᵒᵖ<VAR>S : Subring R<GOAL>x ∈ S.op ↔ MulOpposite.unop x ∈ S
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring Rᵐᵒᵖ<GOAL>S.unop.toSubsemiring = S.unop
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring Rᵐᵒᵖ<GOAL>↑S.unop = MulOpposite.op ⁻¹' ↑S
<VAR>R : Type u_2<VAR>Ring R<VAR>x : R<VAR>S : Subring Rᵐᵒᵖ<GOAL>x ∈ S.unop ↔ MulOpposite.op x ∈ S
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring R<GOAL>S.op.unop = S
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring Rᵐᵒᵖ<GOAL>S.unop.op = S
<VAR>R : Type u_2<VAR>Ring R<VAR>S₁ : Subring R<VAR>S₂ : Subring Rᵐᵒᵖ<GOAL>S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
<VAR>R : Type u_2<VAR>Ring R<VAR>S₁ : Subring Rᵐᵒᵖ<VAR>S₂ : Subring R<GOAL>S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
<VAR>R : Type u_2<VAR>Ring R<VAR>S₁ S₂ : Subring R<GOAL>S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
<VAR>R : Type u_2<VAR>Ring R<VAR>S₁ S₂ : Subring Rᵐᵒᵖ<GOAL>S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring R<GOAL>Subring.opEquiv S = S.op
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring Rᵐᵒᵖ<GOAL>(RelIso.symm Subring.opEquiv) S = S.unop
<VAR>R : Type u_2<VAR>Ring R<GOAL>⊥.op = ⊥
<VAR>R : Type u_2<VAR>Ring R<GOAL>⊥.unop = ⊥
<VAR>R : Type u_2<VAR>Ring R<GOAL>⊤.op = ⊤
<VAR>R : Type u_2<VAR>Ring R<GOAL>⊤.unop = ⊤
<VAR>R : Type u_2<VAR>Ring R<VAR>S₁ S₂ : Subring R<GOAL>(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
<VAR>R : Type u_2<VAR>Ring R<VAR>S₁ S₂ : Subring Rᵐᵒᵖ<GOAL>(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
<VAR>R : Type u_2<VAR>Ring R<VAR>S₁ S₂ : Subring R<GOAL>(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
<VAR>R : Type u_2<VAR>Ring R<VAR>S₁ S₂ : Subring Rᵐᵒᵖ<GOAL>(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Set (Subring R)<GOAL>(sSup S).op = sSup (Subring.unop ⁻¹' S)
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Set (Subring Rᵐᵒᵖ)<GOAL>(sSup S).unop = sSup (Subring.op ⁻¹' S)
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Set (Subring R)<GOAL>(sInf S).op = sInf (Subring.unop ⁻¹' S)
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Set (Subring Rᵐᵒᵖ)<GOAL>(sInf S).unop = sInf (Subring.op ⁻¹' S)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>Ring R<VAR>S : ι → Subring R<GOAL>(iSup S).op = ⨆ i, (S i).op
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>Ring R<VAR>S : ι → Subring Rᵐᵒᵖ<GOAL>(iSup S).unop = ⨆ i, (S i).unop
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>Ring R<VAR>S : ι → Subring R<GOAL>(iInf S).op = ⨅ i, (S i).op
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>Ring R<VAR>S : ι → Subring Rᵐᵒᵖ<GOAL>(iInf S).unop = ⨅ i, (S i).unop
<VAR>R : Type u_2<VAR>Ring R<VAR>s : Set R<GOAL>(Subring.closure s).op = Subring.closure (MulOpposite.unop ⁻¹' s)
<VAR>R : Type u_2<VAR>Ring R<VAR>s : Set Rᵐᵒᵖ<GOAL>(Subring.closure s).unop = Subring.closure (MulOpposite.op ⁻¹' s)
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring R<VAR>b : { b // (fun x => x ∈ S.op) b }<GOAL>↑(S.addEquivOp.symm b) = MulOpposite.unop ↑b
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring R<VAR>a : { a // (fun x => x ∈ S.toSubmonoid) a }<GOAL>↑(S.addEquivOp a) = MulOpposite.op ↑a
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring R<GOAL>∀ (a : ↥S.toSubsemiring), S.ringEquivOpMop a = MulOpposite.op (S.addEquivOp a)
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring R<GOAL>∀ (a : (↥S.op)ᵐᵒᵖ), ↑(S.ringEquivOpMop.symm a) = MulOpposite.unop ↑(MulOpposite.unop a)
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring R<GOAL>∀ (a : (↥S.toSubsemiring)ᵐᵒᵖ), ↑(S.mopRingEquivOp a) = MulOpposite.op ↑(MulOpposite.unop a)
<VAR>R : Type u_2<VAR>Ring R<VAR>S : Subring 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>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a : A<GOAL>↑(LinearMap.mulLeft R a) = AddMonoidHom.mulLeft a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a : A<GOAL>↑(LinearMap.mulRight R a) = AddMonoidHom.mulRight a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a b : A<GOAL>((LinearMap.mul R A) a) b = a * b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a b : A<GOAL>(LinearMap.mulLeft R a) b = a * b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a b : A<GOAL>(LinearMap.mulRight R a) b = b * a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a b x : A<GOAL>(LinearMap.mulLeftRight R (a, b)) x = a * x * b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a b : A<GOAL>(LinearMap.mul' R A) (a ⊗ₜ[R] b) = a * b