ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>CommRing α<VAR>IsDomain α<VAR>NormalizedGCDMonoid α<VAR>a b c : α<VAR>h : a ∣ b - c<GOAL>gcd b a = gcd c a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableEq α<VAR>f : Associates α →* α<VAR>hinv : Function.RightInverse (⇑f) Associates.mk<VAR>a : α<GOAL>a * ↑(Classical.choose ⋯) = f (Associates.mk a)
<VAR>G₀ : Type u_2<VAR>CommGroupWithZero G₀<VAR>DecidableEq G₀<VAR>a : G₀<VAR>h0 : a ≠ 0<GOAL>↑(normUnit a) = a⁻¹
<VAR>G₀ : Type u_2<VAR>CommGroupWithZero G₀<VAR>DecidableEq G₀<VAR>a : G₀<VAR>h0 : a ≠ 0<GOAL>normalize a = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>gcd (Associates.mk a) (Associates.mk b) = Associates.mk (gcd a b)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a b : α<GOAL>lcm (Associates.mk a) (Associates.mk b) = Associates.mk (lcm a b)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.IsPreimmersion f<GOAL>Embedding ⇑f.val.base
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.IsPreimmersion f ↔ Embedding ⇑f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.IsPreimmersion f<VAR>x : ↑↑X.toPresheafedSpace<GOAL>Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>AlgebraicGeometry.IsPreimmersion f<GOAL>Embedding ⇑f.val.base
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>AlgebraicGeometry.IsPreimmersion f<VAR>x : ↑↑X.toPresheafedSpace<GOAL>Function.Surjective ⇑(f.stalkMap x)
<GOAL>@AlgebraicGeometry.IsPreimmersion = (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Embedding) ⊓ AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] x => Function.Surjective ⇑x
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.IsPreimmersion g<VAR>AlgebraicGeometry.IsPreimmersion (f ≫ g)<GOAL>AlgebraicGeometry.IsPreimmersion f
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.IsPreimmersion g<GOAL>AlgebraicGeometry.IsPreimmersion (f ≫ g) ↔ AlgebraicGeometry.IsPreimmersion f
<VAR>R : Type u<VAR>M : Type v<VAR>r : R<VAR>m : M<GOAL>TrivSqZeroExt.fst (r, m) = r
<VAR>R : Type u<VAR>M : Type v<VAR>r : R<VAR>m : M<GOAL>TrivSqZeroExt.snd (r, m) = m
<VAR>R : Type u<VAR>M : Type v<VAR>x y : tsze R M<VAR>h1 : x.fst = y.fst<VAR>h2 : x.snd = y.snd<GOAL>x = y
<VAR>R : Type u<VAR>M : Type v<VAR>Zero M<VAR>r : R<GOAL>(TrivSqZeroExt.inl r).fst = r
<VAR>R : Type u<VAR>M : Type v<VAR>Zero M<VAR>r : R<GOAL>(TrivSqZeroExt.inl r).snd = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Zero M<GOAL>TrivSqZeroExt.fst ∘ TrivSqZeroExt.inl = id
<VAR>R : Type u<VAR>M : Type v<VAR>Zero M<GOAL>TrivSqZeroExt.snd ∘ TrivSqZeroExt.inl = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<VAR>m : M<GOAL>(TrivSqZeroExt.inr m).fst = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<VAR>m : M<GOAL>(TrivSqZeroExt.inr m).snd = m
<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<GOAL>TrivSqZeroExt.fst ∘ TrivSqZeroExt.inr = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<GOAL>TrivSqZeroExt.snd ∘ TrivSqZeroExt.inr = id
<VAR>R : Type u<VAR>M : Type v<VAR>Zero M<GOAL>Function.Injective TrivSqZeroExt.inl
<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<GOAL>Function.Injective TrivSqZeroExt.inr
<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<VAR>Zero M<GOAL>TrivSqZeroExt.fst 0 = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<VAR>Zero M<GOAL>TrivSqZeroExt.snd 0 = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Add R<VAR>Add M<VAR>x₁ x₂ : tsze R M<GOAL>(x₁ + x₂).fst = x₁.fst + x₂.fst
<VAR>R : Type u<VAR>M : Type v<VAR>Add R<VAR>Add M<VAR>x₁ x₂ : tsze R M<GOAL>(x₁ + x₂).snd = x₁.snd + x₂.snd
<VAR>R : Type u<VAR>M : Type v<VAR>Neg R<VAR>Neg M<VAR>x : tsze R M<GOAL>(-x).fst = -x.fst
<VAR>R : Type u<VAR>M : Type v<VAR>Neg R<VAR>Neg M<VAR>x : tsze R M<GOAL>(-x).snd = -x.snd
<VAR>R : Type u<VAR>M : Type v<VAR>Sub R<VAR>Sub M<VAR>x₁ x₂ : tsze R M<GOAL>(x₁ - x₂).fst = x₁.fst - x₂.fst
<VAR>R : Type u<VAR>M : Type v<VAR>Sub R<VAR>Sub M<VAR>x₁ x₂ : tsze R M<GOAL>(x₁ - x₂).snd = x₁.snd - x₂.snd
<VAR>S : Type u_2<VAR>R : Type u<VAR>M : Type v<VAR>SMul S R<VAR>SMul S M<VAR>s : S<VAR>x : tsze R M<GOAL>(s •> x).fst = s •> x.fst
<VAR>S : Type u_2<VAR>R : Type u<VAR>M : Type v<VAR>SMul S R<VAR>SMul S M<VAR>s : S<VAR>x : tsze R M<GOAL>(s •> x).snd = s •> x.snd
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type u_3<VAR>AddCommMonoid R<VAR>AddCommMonoid M<VAR>s : Finset ι<VAR>f : ι → tsze R M<GOAL>(∑ i ∈ s, f i).fst = ∑ i ∈ s, (f i).fst
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type u_3<VAR>AddCommMonoid R<VAR>AddCommMonoid M<VAR>s : Finset ι<VAR>f : ι → tsze R M<GOAL>(∑ i ∈ s, f i).snd = ∑ i ∈ s, (f i).snd
<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<VAR>Zero M<GOAL>TrivSqZeroExt.inl 0 = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Add R<VAR>AddZeroClass M<VAR>r₁ r₂ : R<GOAL>TrivSqZeroExt.inl (r₁ + r₂) = TrivSqZeroExt.inl r₁ + TrivSqZeroExt.inl r₂
<VAR>R : Type u<VAR>M : Type v<VAR>Neg R<VAR>SubNegZeroMonoid M<VAR>r : R<GOAL>TrivSqZeroExt.inl (-r) = -TrivSqZeroExt.inl r
<VAR>R : Type u<VAR>M : Type v<VAR>Sub R<VAR>SubNegZeroMonoid M<VAR>r₁ r₂ : R<GOAL>TrivSqZeroExt.inl (r₁ - r₂) = TrivSqZeroExt.inl r₁ - TrivSqZeroExt.inl r₂
<VAR>S : Type u_2<VAR>R : Type u<VAR>M : Type v<VAR>Monoid S<VAR>AddMonoid M<VAR>SMul S R<VAR>DistribMulAction S M<VAR>s : S<VAR>r : R<GOAL>TrivSqZeroExt.inl (s •> r) = s •> TrivSqZeroExt.inl r
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type u_3<VAR>AddCommMonoid R<VAR>AddCommMonoid M<VAR>s : Finset ι<VAR>f : ι → R<GOAL>TrivSqZeroExt.inl (∑ i ∈ s, f i) = ∑ i ∈ s, TrivSqZeroExt.inl (f i)
<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<VAR>Zero M<GOAL>TrivSqZeroExt.inr 0 = 0
<VAR>R : Type u<VAR>M : Type v<VAR>AddZeroClass R<VAR>AddZeroClass M<VAR>m₁ m₂ : M<GOAL>TrivSqZeroExt.inr (m₁ + m₂) = TrivSqZeroExt.inr m₁ + TrivSqZeroExt.inr m₂
<VAR>R : Type u<VAR>M : Type v<VAR>SubNegZeroMonoid R<VAR>Neg M<VAR>m : M<GOAL>TrivSqZeroExt.inr (-m) = -TrivSqZeroExt.inr m
<VAR>R : Type u<VAR>M : Type v<VAR>SubNegZeroMonoid R<VAR>Sub M<VAR>m₁ m₂ : M<GOAL>TrivSqZeroExt.inr (m₁ - m₂) = TrivSqZeroExt.inr m₁ - TrivSqZeroExt.inr m₂
<VAR>S : Type u_2<VAR>R : Type u<VAR>M : Type v<VAR>Zero R<VAR>Zero S<VAR>SMulWithZero S R<VAR>SMul S M<VAR>r : S<VAR>m : M<GOAL>TrivSqZeroExt.inr (r •> m) = r •> TrivSqZeroExt.inr m
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type u_3<VAR>AddCommMonoid R<VAR>AddCommMonoid M<VAR>s : Finset ι<VAR>f : ι → M<GOAL>TrivSqZeroExt.inr (∑ i ∈ s, f i) = ∑ i ∈ s, TrivSqZeroExt.inr (f i)
<VAR>R : Type u<VAR>M : Type v<VAR>AddZeroClass R<VAR>AddZeroClass M<VAR>x : tsze R M<GOAL>TrivSqZeroExt.inl x.fst + TrivSqZeroExt.inr x.snd = x
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>AddZeroClass R<VAR>AddZeroClass M<VAR>P : tsze R M → Prop<VAR>inl_add_inr : ∀ (r : R) (m : M), P (TrivSqZeroExt.inl r + TrivSqZeroExt.inr m)<VAR>x : tsze R M<GOAL>P x
<VAR>S : Type u_2<VAR>R : Type u<VAR>M : Type v<VAR>N : Type u_3<VAR>Semiring S<VAR>AddCommMonoid R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module S R<VAR>Module S M<VAR>Module S N<VAR>f g : tsze R M →ₗ[S] N<VAR>hl : ∀ (r : R), f (TrivSqZeroExt.inl r) = g (TrivSqZeroExt.inl r)<VAR>hr : ∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.inr m)<GOAL>f = g
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<GOAL>(TrivSqZeroExt.inrHom R M) m = TrivSqZeroExt.inr m
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : tsze R M<GOAL>(TrivSqZeroExt.sndHom R M) x = x.snd
<VAR>R : Type u<VAR>M : Type v<VAR>One R<VAR>Zero M<GOAL>TrivSqZeroExt.fst 1 = 1
<VAR>R : Type u<VAR>M : Type v<VAR>One R<VAR>Zero M<GOAL>TrivSqZeroExt.snd 1 = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Mul R<VAR>Add M<VAR>SMul R M<VAR>SMul Rᵐᵒᵖ M<VAR>x₁ x₂ : tsze R M<GOAL>(x₁ * x₂).fst = x₁.fst * x₂.fst
<VAR>R : Type u<VAR>M : Type v<VAR>Mul R<VAR>Add M<VAR>SMul R M<VAR>SMul Rᵐᵒᵖ M<VAR>x₁ x₂ : tsze R M<GOAL>(x₁ * x₂).snd = x₁.fst •> x₂.snd + x₁.snd <• x₂.fst
<VAR>R : Type u<VAR>M : Type v<VAR>One R<VAR>Zero M<GOAL>TrivSqZeroExt.inl 1 = 1
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>r₁ r₂ : R<GOAL>TrivSqZeroExt.inl (r₁ * r₂) = TrivSqZeroExt.inl r₁ * TrivSqZeroExt.inl r₂
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>r₁ r₂ : R<GOAL>TrivSqZeroExt.inl r₁ * TrivSqZeroExt.inl r₂ = TrivSqZeroExt.inl (r₁ * r₂)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>m₁ m₂ : M<GOAL>TrivSqZeroExt.inr m₁ * TrivSqZeroExt.inr m₂ = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>r : R<VAR>m : M<GOAL>TrivSqZeroExt.inl r * TrivSqZeroExt.inr m = TrivSqZeroExt.inr (r •> m)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>r : R<VAR>m : M<GOAL>TrivSqZeroExt.inr m * TrivSqZeroExt.inl r = TrivSqZeroExt.inr (m <• r)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>r : R<VAR>x : tsze R M<GOAL>TrivSqZeroExt.inl r * x = r •> x
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>r : R<GOAL>x * TrivSqZeroExt.inl r = x <• r
<VAR>R : Type u<VAR>M : Type v<VAR>AddMonoidWithOne R<VAR>AddMonoid M<VAR>n : ℕ<GOAL>(↑n).fst = ↑n
<VAR>R : Type u<VAR>M : Type v<VAR>AddMonoidWithOne R<VAR>AddMonoid M<VAR>n : ℕ<GOAL>(↑n).snd = 0
<VAR>R : Type u<VAR>M : Type v<VAR>AddMonoidWithOne R<VAR>AddMonoid M<VAR>n : ℕ<GOAL>TrivSqZeroExt.inl ↑n = ↑n
<VAR>R : Type u<VAR>M : Type v<VAR>AddGroupWithOne R<VAR>AddGroup M<VAR>z : ℤ<GOAL>(↑z).fst = ↑z
<VAR>R : Type u<VAR>M : Type v<VAR>AddGroupWithOne R<VAR>AddGroup M<VAR>z : ℤ<GOAL>(↑z).snd = 0
<VAR>R : Type u<VAR>M : Type v<VAR>AddGroupWithOne R<VAR>AddGroup M<VAR>z : ℤ<GOAL>TrivSqZeroExt.inl ↑z = ↑z
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>n : ℕ<GOAL>(x ^ n).fst = x.fst ^ n
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>n : ℕ<GOAL>(x ^ n).snd = (List.map (fun i => x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i) (List.range n)).sum
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>n : ℕ<VAR>h : x.snd <• x.fst = x.fst •> x.snd<GOAL>(x ^ n).snd = n •> x.fst ^ n.pred •> x.snd
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>h : x.snd <• x.fst = x.fst •> x.snd<VAR>n : ℕ<GOAL>x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>n : ℕ<VAR>h : x.snd <• x.fst = x.fst •> x.snd<GOAL>(x ^ n).snd = n •> (x.snd <• x.fst ^ n.pred)
<VAR>R : Type u<VAR>M : Type v<VAR>CommMonoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>IsCentralScalar R M<VAR>x : tsze R M<VAR>n : ℕ<GOAL>(x ^ n).snd = n •> x.fst ^ n.pred •> x.snd
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>r : R<VAR>n : ℕ<GOAL>TrivSqZeroExt.inl r ^ n = TrivSqZeroExt.inl (r ^ n)
<VAR>R : Type u<VAR>M : Type v<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>DistribMulAction Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>l : List (tsze R M)<GOAL>l.prod.fst = (List.map TrivSqZeroExt.fst l).prod
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>l : List (tsze R M)<GOAL>l.prod.snd = (List.map (fun x => (List.take x.1 (List.map TrivSqZeroExt.fst l)).prod •> x.2.snd <• (List.drop x.1.succ (List.map TrivSqZeroExt.fst l)).prod) l.enum).sum
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>r : R<GOAL>(TrivSqZeroExt.inlHom R M) r = TrivSqZeroExt.inl r
<VAR>R : Type u<VAR>M : Type v<VAR>Neg M<VAR>Inv R<VAR>SMul Rᵐᵒᵖ M<VAR>SMul R M<VAR>x : tsze R M<GOAL>x⁻¹.fst = x.fst⁻¹
<VAR>R : Type u<VAR>M : Type v<VAR>Neg M<VAR>Inv R<VAR>SMul Rᵐᵒᵖ M<VAR>SMul R M<VAR>x : tsze R M<GOAL>x⁻¹.snd = -(x.fst⁻¹ •> x.snd <• x.fst⁻¹)
<VAR>R : Type u<VAR>M : Type v<VAR>DivisionSemiring R<VAR>AddCommGroup M<VAR>Module Rᵐᵒᵖ M<VAR>Module R M<VAR>r : R<GOAL>(TrivSqZeroExt.inl r)⁻¹ = TrivSqZeroExt.inl r⁻¹
<VAR>R : Type u<VAR>M : Type v<VAR>DivisionSemiring R<VAR>AddCommGroup M<VAR>Module Rᵐᵒᵖ M<VAR>Module R M<VAR>m : M<GOAL>(TrivSqZeroExt.inr m)⁻¹ = 0
<VAR>R : Type u<VAR>M : Type v<VAR>DivisionSemiring R<VAR>AddCommGroup M<VAR>Module Rᵐᵒᵖ M<VAR>Module R M<GOAL>0⁻¹ = 0
<VAR>R : Type u<VAR>M : Type v<VAR>DivisionSemiring R<VAR>AddCommGroup M<VAR>Module Rᵐᵒᵖ M<VAR>Module R M<GOAL>1⁻¹ = 1
<VAR>R : Type u<VAR>M : Type v<VAR>DivisionSemiring R<VAR>AddCommGroup M<VAR>Module Rᵐᵒᵖ M<VAR>Module R M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : x.fst ≠ 0<GOAL>x * x⁻¹ = 1
<VAR>R : Type u<VAR>M : Type v<VAR>DivisionSemiring R<VAR>AddCommGroup M<VAR>Module Rᵐᵒᵖ M<VAR>Module R M<VAR>x : tsze R M<VAR>hx : x.fst ≠ 0<GOAL>x⁻¹ * x = 1
<VAR>R : Type u<VAR>M : Type v<VAR>DivisionSemiring R<VAR>AddCommGroup M<VAR>Module Rᵐᵒᵖ M<VAR>Module R M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>a b : tsze R M<GOAL>(a * b)⁻¹ = b⁻¹ * a⁻¹
<VAR>R : Type u<VAR>M : Type v<VAR>DivisionSemiring R<VAR>AddCommGroup M<VAR>Module Rᵐᵒᵖ M<VAR>Module R M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : x.fst ≠ 0<GOAL>x⁻¹⁻¹ = x
<VAR>R : Type u<VAR>M : Type v<VAR>DivisionRing R<VAR>AddCommGroup M<VAR>Module Rᵐᵒᵖ M<VAR>Module R M<VAR>x : tsze R M<GOAL>(-x)⁻¹ = -x⁻¹
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<GOAL>⇑(algebraMap R' (tsze R' M)) = TrivSqZeroExt.inl
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<GOAL>algebraMap R' (tsze R' M) = TrivSqZeroExt.inlHom R' M
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>s : S<GOAL>(algebraMap S (tsze R M)) s = TrivSqZeroExt.inl ((algebraMap S R) s)
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>x : tsze R M<GOAL>(TrivSqZeroExt.fstHom S R M) x = x.fst
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>r : R<GOAL>(TrivSqZeroExt.inlAlgHom S R M) r = TrivSqZeroExt.inl r
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R' A<VAR>f g : tsze R' M →ₐ[R'] A<VAR>h : ∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.inr m)<GOAL>f = g
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>f g : tsze R M →ₐ[S] A<VAR>hinl : f.comp (TrivSqZeroExt.inlAlgHom S R M) = g.comp (TrivSqZeroExt.inlAlgHom S R M)<VAR>hinr : f.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M) = g.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M)<GOAL>f = g
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>f : R →ₐ[S] A<VAR>g : M →ₗ[S] A<VAR>hg : ∀ (x y : M), g x * g y = 0<VAR>hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x<VAR>hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r<VAR>x : tsze R M<GOAL>(TrivSqZeroExt.lift f g hg hfg hgf) x = f x.fst + g x.snd
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>f : R →ₐ[S] A<VAR>g : M →ₗ[S] A<VAR>hg : ∀ (x y : M), g x * g y = 0<VAR>hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x<VAR>hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r<VAR>r : R<GOAL>(TrivSqZeroExt.lift f g hg hfg hgf) (TrivSqZeroExt.inl r) = f r
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>f : R →ₐ[S] A<VAR>g : M →ₗ[S] A<VAR>hg : ∀ (x y : M), g x * g y = 0<VAR>hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x<VAR>hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r<VAR>m : M<GOAL>(TrivSqZeroExt.lift f g hg hfg hgf) (TrivSqZeroExt.inr m) = g m
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>f : R →ₐ[S] A<VAR>g : M →ₗ[S] A<VAR>hg : ∀ (x y : M), g x * g y = 0<VAR>hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x<VAR>hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r<GOAL>(TrivSqZeroExt.lift f g hg hfg hgf).comp (TrivSqZeroExt.inlAlgHom S R M) = f
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>f : R →ₐ[S] A<VAR>g : M →ₗ[S] A<VAR>hg : ∀ (x y : M), g x * g y = 0<VAR>hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x<VAR>hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r<GOAL>(TrivSqZeroExt.lift f g hg hfg hgf).toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M) = g
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<GOAL>TrivSqZeroExt.lift (TrivSqZeroExt.inlAlgHom S R M) (↑S (TrivSqZeroExt.inrHom R M)) ⋯ ⋯ ⋯ = AlgHom.id S (tsze R M)
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>fg : { fg // (∀ (x y : M), fg.2 x * fg.2 y = 0) ∧ (∀ (r : R) (x : M), fg.2 (r •> x) = fg.1 r * fg.2 x) ∧ ∀ (r : R) (x : M), fg.2 (x <• r) = fg.2 x * fg.1 r }<GOAL>TrivSqZeroExt.liftEquiv fg = TrivSqZeroExt.lift (↑fg).1 (↑fg).2 ⋯ ⋯ ⋯
<VAR>S : Type u_1<VAR>R : Type u<VAR>M : Type v<VAR>CommSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Algebra S R<VAR>Module S M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>SMulCommClass R Rᵐᵒᵖ M<VAR>IsScalarTower S R M<VAR>IsScalarTower S Rᵐᵒᵖ M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>F : tsze R M →ₐ[S] A<GOAL>↑(TrivSqZeroExt.liftEquiv.symm F) = (F.comp (TrivSqZeroExt.inlAlgHom S R M), F.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M))
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R' A<GOAL>∀ (a : tsze R' M →ₐ[R'] A), ↑(TrivSqZeroExt.liftEquivOfComm.symm a) = a.toLinearMap ∘ₗ ↑R' (TrivSqZeroExt.inrHom R' M)
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R' A<GOAL>∀ (a : { f // ∀ (x y : M), f x * f y = 0 }), TrivSqZeroExt.liftEquivOfComm a = TrivSqZeroExt.lift (Algebra.ofId R' A) ↑a ⋯ ⋯ ⋯
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R' N<VAR>Module R'ᵐᵒᵖ N<VAR>IsCentralScalar R' N<VAR>f : M →ₗ[R'] N<VAR>r : R'<GOAL>(TrivSqZeroExt.map f) (TrivSqZeroExt.inl r) = TrivSqZeroExt.inl r
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R' N<VAR>Module R'ᵐᵒᵖ N<VAR>IsCentralScalar R' N<VAR>f : M →ₗ[R'] N<VAR>x : M<GOAL>(TrivSqZeroExt.map f) (TrivSqZeroExt.inr x) = TrivSqZeroExt.inr (f x)
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R' N<VAR>Module R'ᵐᵒᵖ N<VAR>IsCentralScalar R' N<VAR>f : M →ₗ[R'] N<VAR>x : tsze R' M<GOAL>((TrivSqZeroExt.map f) x).fst = x.fst
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R' N<VAR>Module R'ᵐᵒᵖ N<VAR>IsCentralScalar R' N<VAR>f : M →ₗ[R'] N<VAR>x : tsze R' M<GOAL>((TrivSqZeroExt.map f) x).snd = f x.snd
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R' N<VAR>Module R'ᵐᵒᵖ N<VAR>IsCentralScalar R' N<VAR>f : M →ₗ[R'] N<GOAL>(TrivSqZeroExt.map f).comp (TrivSqZeroExt.inlAlgHom R' R' M) = TrivSqZeroExt.inlAlgHom R' R' N
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R' N<VAR>Module R'ᵐᵒᵖ N<VAR>IsCentralScalar R' N<VAR>f : M →ₗ[R'] N<GOAL>(TrivSqZeroExt.map f).toLinearMap ∘ₗ TrivSqZeroExt.inrHom R' M = TrivSqZeroExt.inrHom R' N ∘ₗ f
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R' N<VAR>Module R'ᵐᵒᵖ N<VAR>IsCentralScalar R' N<VAR>f : M →ₗ[R'] N<GOAL>(TrivSqZeroExt.fstHom R' R' N).comp (TrivSqZeroExt.map f) = TrivSqZeroExt.fstHom R' R' M
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R' N<VAR>Module R'ᵐᵒᵖ N<VAR>IsCentralScalar R' N<VAR>f : M →ₗ[R'] N<GOAL>TrivSqZeroExt.sndHom R' N ∘ₗ (TrivSqZeroExt.map f).toLinearMap = f ∘ₗ TrivSqZeroExt.sndHom R' M
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<GOAL>TrivSqZeroExt.map LinearMap.id = AlgHom.id R' (tsze R' M)
<VAR>R' : Type u<VAR>M : Type v<VAR>CommSemiring R'<VAR>AddCommMonoid M<VAR>Module R' M<VAR>Module R'ᵐᵒᵖ M<VAR>IsCentralScalar R' M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>AddCommMonoid N<VAR>Module R' N<VAR>Module R'ᵐᵒᵖ N<VAR>IsCentralScalar R' N<VAR>AddCommMonoid P<VAR>Module R' P<VAR>Module R'ᵐᵒᵖ P<VAR>IsCentralScalar R' P<VAR>f : M →ₗ[R'] N<VAR>g : N →ₗ[R'] P<GOAL>TrivSqZeroExt.map (g ∘ₗ f) = (TrivSqZeroExt.map g).comp (TrivSqZeroExt.map f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>self : AlgebraicGeometry.IsLocallyNoetherian X<VAR>U : ↑X.affineOpens<GOAL>IsNoetherianRing ↑Γ(X, ↑U)