import UnitConjecture.FreeModule /-! # Group Rings We construct the Group ring `R[G]` given a group `G` and a ring `R`, both having decidable equality. The ring structures is constructed using the (implicit) universal property of `R`-modules. As a check on our definitions, `R[G]` is proved to be a Ring. We first define multiplication on formal sums. We prove many properties that are used both to show invariance under elementary moves and to prove that `R[G]` is a ring. -/ variable {R :R: TypeType} [RingType: Type 1R] [DecidableEqR: TypeR] variable {R: TypeG:G: TypeType} [GroupType: Type 1G] [DecidableEqG: TypeG] /-! ## Multiplication on formal sums -/ section FormalSumMul /-- multiplication by a monomial -/ def FormalSum.mulMonom (G: Typeb:b: RR)(R: Typeh:h: GG) : FormalSumG: TypeRR: TypeG → FormalSumG: TypeRR: TypeG | [] =>G: Type[] | ([]: List ?m.109a,a: Rg) :: tail => (g: Ga *a: Rb,b: Rg *g: Gh) :: (mulMonomh: Gbb: Rh tail) /-- multiplication for formal sums -/ defh: GFormalSum.mul(fst: FormalSumfst: FormalSum R GRR: TypeG) : FormalSumG: TypeRR: TypeG → FormalSumG: TypeRR: TypeG | [] =>G: Type[] | ([]: List ?m.1236b,b: Rh) :: ys => (FormalSum.mulMonomh: Gbb: Rhh: Gfst) ++ (mulfst: FormalSum R Gfst ys) end FormalSumMul /-! ## Properties of multiplication on formal sums -/ namespace GroupRing open FormalSum /-- multiplication by the zero monomial -/ theoremfst: FormalSum R Gmul_monom_zero (gg: Gx₀:x₀: GG)(G: Types: FormalSums: FormalSum R GRR: TypeG):G: Typecoords (mulMonomcoords: {R : Type ?u.1748} → [inst : Ring R] → {X : Type ?u.1747} → [inst_1 : DecidableEq X] → FormalSum R X → X → R00: ?m.1766gg: Gs)s: FormalSum R Gx₀ =x₀: G0 :=0: ?m.1876R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
g, x₀: G
s: FormalSum R GR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
g, x₀: G
s: FormalSum R G
nilGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
g, x₀: G
s: FormalSum R G/-- distributivity of multiplication by a monomial -/ theoremGoals accomplished! 🐙mul_monom_dist(b :b: RR)(R: Typehh: Gx₀ :x₀: GG)(G: Types₁s₁: FormalSum R Gs₂: FormalSums₂: FormalSum R GRR: TypeG):G: Typecoords (mulMonomcoords: {R : Type ?u.4031} → [inst : Ring R] → {X : Type ?u.4030} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rbb: Rh (h: Gs₁ ++s₁: FormalSum R Gs₂))s₂: FormalSum R Gx₀ =x₀: Gcoords (mulMonomcoords: {R : Type ?u.4136} → [inst : Ring R] → {X : Type ?u.4135} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rbb: Rhh: Gs₁)s₁: FormalSum R Gx₀ +x₀: Gcoords (mulMonomcoords: {R : Type ?u.4157} → [inst : Ring R] → {X : Type ?u.4156} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rbb: Rhh: Gs₂)s₂: FormalSum R Gx₀ :=x₀: GGoals accomplished! 🐙/-- right distributivity -/ theoremGoals accomplished! 🐙mul_dist(x₀ :x₀: GG)(G: Types₁s₁: FormalSum R Gs₂s₂: FormalSum R Gs₃: FormalSums₃: FormalSum R GRR: TypeG):G: Typecoords (mulcoords: {R : Type ?u.6477} → [inst : Ring R] → {X : Type ?u.6476} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rs₁ (s₁: FormalSum R Gs₂ ++s₂: FormalSum R Gs₃))s₃: FormalSum R Gx₀ =x₀: Gcoords (mulcoords: {R : Type ?u.6582} → [inst : Ring R] → {X : Type ?u.6581} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rs₁s₁: FormalSum R Gs₂)s₂: FormalSum R Gx₀ +x₀: Gcoords (mulcoords: {R : Type ?u.6603} → [inst : Ring R] → {X : Type ?u.6602} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rs₁s₁: FormalSum R Gs₃)s₃: FormalSum R Gx₀ :=x₀: GGoals accomplished! 🐙/-- associativity with two terms monomials -/ theoremGoals accomplished! 🐙mul_monom_monom_assoc(aa: Rb :b: RR)(R: Typehh: Gx₀ :x₀: GG)(G: Types : FormalSums: FormalSum R GRR: TypeG):G: Typecoords (mulMonomcoords: {R : Type ?u.8812} → [inst : Ring R] → {X : Type ?u.8811} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rbb: Rh (mulMonomh: Gaa: Rxx: ?m.8794s))s: FormalSum R Gx₀ =x₀: Gcoords (mulMonom (coords: {R : Type ?u.8877} → [inst : Ring R] → {X : Type ?u.8876} → [inst_1 : DecidableEq X] → FormalSum R X → X → Ra *a: Rb) (b: Rx *x: ?m.8794h)h: Gs)s: FormalSum R Gx₀ :=x₀: GGoals accomplished! 🐙/-- associativity with one term a monomial -/ theoremGoals accomplished! 🐙mul_monom_assoc(b :b: RR)(R: Typehh: Gx₀ :x₀: GG)(G: Types₁s₁: FormalSum R Gs₂: FormalSums₂: FormalSum R GRR: TypeG):G: Typecoords (mulMonomcoords: {R : Type ?u.11330} → [inst : Ring R] → {X : Type ?u.11329} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rbb: Rh (mulh: Gs₁s₁: FormalSum R Gs₂))s₂: FormalSum R Gx₀ =x₀: Gcoords (mulcoords: {R : Type ?u.11399} → [inst : Ring R] → {X : Type ?u.11398} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rs₁ (mulMonoms₁: FormalSum R Gbb: Rhh: Gs₂))s₂: FormalSum R Gx₀ :=x₀: GGoals accomplished! 🐙/-- left distributivity for multiplication by a monomial -/ theoremGoals accomplished! 🐙mul_monom_add(b₁b₁: Rb₂ :b₂: RR)(R: Typehh: Gx₀ :x₀: GG)(G: Types: FormalSums: FormalSum R GRR: TypeG):G: Typecoords (mulMonom (coords: {R : Type ?u.14108} → [inst : Ring R] → {X : Type ?u.14107} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rb₁ +b₁: Rb₂)b₂: Rhh: Gs)s: FormalSum R Gx₀ =x₀: Gcoords (mulMonomcoords: {R : Type ?u.14257} → [inst : Ring R] → {X : Type ?u.14256} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rb₁b₁: Rhh: Gs)s: FormalSum R Gx₀ +x₀: Gcoords (mulMonomcoords: {R : Type ?u.14278} → [inst : Ring R] → {X : Type ?u.14277} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rb₂b₂: Rhh: Gs)s: FormalSum R Gx₀ :=x₀: GGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
a/-- multiplication equivalent when adding term with `0` coefficient -/ theorem mul_zero_cons (R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b₁, b₂: R
h, x₀: G
head: R × G
tail: List (R × G)
ih: coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a: R
g: G
ass: FormalSum R Gt : FormalSumt: FormalSum R GRR: TypeG) : mulG: Types ((s: FormalSum R G0,0: ?m.18238h) ::h: ?m.18198t) ≈ mult: FormalSum R Gss: FormalSum R Gt :=t: FormalSum R GR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: G
t: FormalSum R GGoals accomplished! 🐙/-! ## Induced product on the quotient -/ /-- Quotient in second argument for group ring multiplication -/ def mulAux : FormalSumGoals accomplished! 🐙RR: TypeG →G: TypeR[R: TypeG] →G: TypeR[R: TypeG] :=G: TypeR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s: FormalSum R G∀ (a b : FormalSum R G), a ≈ b → Quotient.mk (formalSumSetoid R G) (mul s a) = Quotient.mk (formalSumSetoid R G) (mul s b)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s: FormalSum R G
a∀ (s₁ s₂ : FormalSum R G), ElementaryMove R G s₁ s₂ → Quotient.mk (formalSumSetoid R G) (mul s s₁) = Quotient.mk (formalSumSetoid R G) (mul s s₂)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
rel: ElementaryMove R G t t'
aQuotient.mk (formalSumSetoid R G) (mul s t) = Quotient.mk (formalSumSetoid R G) (mul s t')R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
rel: ElementaryMove R G t t'
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
rel: ElementaryMove R G t t'
aGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
rel: ElementaryMove R G t t'
aGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
rel: ElementaryMove R G t t'
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a: R
x: G
s₁, s₂: FormalSum R G
a✝: ElementaryMove R G s₁ s₂
step: mul s s₁ ≈ mul s s₂
x₀: G
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a: R
x: G
s₁, s₂: FormalSum R G
a✝: ElementaryMove R G s₁ s₂
step: mul s s₁ ≈ mul s s₂
x₀: G
a.cons.hGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
rel: ElementaryMove R G t t'
aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
a.swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
a.swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
a.swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
a.swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
a.swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
a.swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
a.swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
lc:= add_comm (coords (mulMonom a₁ x₁ s) x₀) (coords (mulMonom a₂ x₂ s) x₀): coords (mulMonom a₁ x₁ s) x₀ + coords (mulMonom a₂ x₂ s) x₀ = coords (mulMonom a₂ x₂ s) x₀ + coords (mulMonom a₁ x₁ s) x₀
a.swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
lc:= add_comm (coords (mulMonom a₁ x₁ s) x₀) (coords (mulMonom a₂ x₂ s) x₀): coords (mulMonom a₁ x₁ s) x₀ + coords (mulMonom a₂ x₂ s) x₀ = coords (mulMonom a₂ x₂ s) x₀ + coords (mulMonom a₁ x₁ s) x₀
a.swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s, t, t': FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
lc:= add_comm (coords (mulMonom a₁ x₁ s) x₀) (coords (mulMonom a₂ x₂ s) x₀): coords (mulMonom a₁ x₁ s) x₀ + coords (mulMonom a₂ x₂ s) x₀ = coords (mulMonom a₂ x₂ s) x₀ + coords (mulMonom a₁ x₁ s) x₀
a.swap.hopen ElementaryMove /-- invariance under moves of multiplication by monomials -/ theoremGoals accomplished! 🐙mul_monom_invariant (b :b: RR)(R: Typehh: Gx₀ :x₀: GG)(G: Types₁s₁: FormalSum R Gs₂ : FormalSums₂: FormalSum R GRR: TypeG) (G: Typerel :rel: ElementaryMove R G s₁ s₂ElementaryMoveElementaryMove: (R X : Type) → [inst : Ring R] → [inst_1 : DecidableEq R] → [inst_2 : DecidableEq X] → FormalSum R X → FormalSum R X → PropRR: TypeGG: Types₁s₁: FormalSum R Gs₂) :s₂: FormalSum R Gcoords (mulMonomcoords: {R : Type ?u.26725} → [inst : Ring R] → {X : Type ?u.26724} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rbb: Rhh: Gs₁)s₁: FormalSum R Gx₀ =x₀: Gcoords (mulMonomcoords: {R : Type ?u.26750} → [inst : Ring R] → {X : Type ?u.26749} → [inst_1 : DecidableEq X] → FormalSum R X → X → Rbb: Rhh: Gs₂)s₂: FormalSum R Gx₀ :=x₀: GR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a: R
x: G
t₁, t₂: FormalSum R G
a✝: ElementaryMove R G t₁ t₂
step: coords (mulMonom b h t₁) x₀ = coords (mulMonom b h t₂) x₀
consGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
swapR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GmonomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
swapR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GmonomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GmonomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GmonomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GmonomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GmonomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R GmonomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
swapR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
b: R
h, x₀: G
s₁, s₂: FormalSum R G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
swap/-- invariance under moves for the first argument for multipilication -/ theoremGoals accomplished! 🐙first_arg_invariant (first_arg_invariant: ∀ {R : Type} [inst : Ring R] [inst_1 : DecidableEq R] {G : Type} [inst_2 : Group G] [inst_3 : DecidableEq G] (s₁ s₂ t : FormalSum R G), ElementaryMove R G s₁ s₂ → mul s₁ t ≈ mul s₂ ts₁s₁: FormalSum R Gs₂s₂: FormalSum R Gt : FormalSumt: FormalSum R GRR: TypeG) (G: Typerel :rel: ElementaryMove R G s₁ s₂ElementaryMoveElementaryMove: (R X : Type) → [inst : Ring R] → [inst_1 : DecidableEq R] → [inst_2 : DecidableEq X] → FormalSum R X → FormalSum R X → PropRR: TypeGG: Types₁s₁: FormalSum R Gs₂) : FormalSum.muls₂: FormalSum R Gs₁s₁: FormalSum R Gt ≈ FormalSum.mult: FormalSum R Gs₂s₂: FormalSum R Gt :=t: FormalSum R GR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂, t: FormalSum R G
rel: ElementaryMove R G s₁ s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
nilR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
head✝: R × G
tail✝: List (R × G)
consR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂, t: FormalSum R G
rel: ElementaryMove R G s₁ s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂[] ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂, t: FormalSum R G
rel: ElementaryMove R G s₁ s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
tail: FormalSum R G
g: G
a: R
hyp: a = 0
x₀: GElementaryMove R G ((0, g) :: tail) tailR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
tail: FormalSum R G
g: G
a: R
hyp: a = 0
x₀: GElementaryMove R G ((0, g) :: tail) tailGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
tail: FormalSum R G
g: G
a: R
hyp: a = 0
x₀: G
rel':= zeroCoeff tail g 0 (Eq.refl 0): ElementaryMove R G ((0, g) :: tail) tail
prev:= first_arg_invariant ((0, g) :: tail) tail tail' rel': mul ((0, g) :: tail) tail' ≈ mul tail tail'
zeroCoeff.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
tail: FormalSum R G
g: G
a: R
hyp: a = 0
x₀: G
rel':= zeroCoeff tail g 0 (Eq.refl 0): ElementaryMove R G ((0, g) :: tail) tail
prev:= first_arg_invariant ((0, g) :: tail) tail tail' rel': mul ((0, g) :: tail) tail' ≈ mul tail tail'
pl:= congrFun prev x₀: coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀
zeroCoeff.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
tail: FormalSum R G
g: G
a: R
hyp: a = 0
x₀: G
rel':= zeroCoeff tail g 0 (Eq.refl 0): ElementaryMove R G ((0, g) :: tail) tail
prev:= first_arg_invariant ((0, g) :: tail) tail tail' rel': mul ((0, g) :: tail) tail' ≈ mul tail tail'
pl:= congrFun prev x₀: coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀
zeroCoeff.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
tail: FormalSum R G
g: G
a: R
hyp: a = 0
x₀: G
rel':= zeroCoeff tail g 0 (Eq.refl 0): ElementaryMove R G ((0, g) :: tail) tail
prev:= first_arg_invariant ((0, g) :: tail) tail tail' rel': mul ((0, g) :: tail) tail' ≈ mul tail tail'
pl:= congrFun prev x₀: coords (mul ((0, g) :: tail) tail') x₀ = coords (mul tail tail') x₀
zeroCoeff.hGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x: G
tail: FormalSum R G
x₀: G
addCoeffs.hmonomCoeff R G x₀ (a₁ * b, x * h) + (monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = monomCoeff R G x₀ (a₁ * b, x * h) + monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀ + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x: G
tail: FormalSum R G
x₀: G
addCoeffs.hmonomCoeff R G x₀ (a₁ * b, x * h) + (monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = monomCoeff R G x₀ (a₁ * b, x * h) + monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀ + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x: G
tail: FormalSum R G
x₀: G
rel':= addCoeffs a₁ a₂ x tail: ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail)
prev:= first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel': mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail'
addCoeffs.hmonomCoeff R G x₀ (a₁ * b, x * h) + (monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = monomCoeff R G x₀ (a₁ * b, x * h) + monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀ + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x: G
tail: FormalSum R G
x₀: G
rel':= addCoeffs a₁ a₂ x tail: ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail)
prev:= first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel': mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = coords (mul ((a₁ + a₂, x) :: tail) tail') x₀
addCoeffs.hmonomCoeff R G x₀ (a₁ * b, x * h) + (monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = monomCoeff R G x₀ (a₁ * b, x * h) + monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀ + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x: G
tail: FormalSum R G
x₀: G
rel':= addCoeffs a₁ a₂ x tail: ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail)
prev:= first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel': mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = coords (mul ((a₁ + a₂, x) :: tail) tail') x₀
addCoeffs.hmonomCoeff R G x₀ (a₁ * b, x * h) + (monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = monomCoeff R G x₀ (a₁ * b, x * h) + monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀ + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x: G
tail: FormalSum R G
x₀: G
rel':= addCoeffs a₁ a₂ x tail: ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail)
prev:= first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel': mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = coords (mul ((a₁ + a₂, x) :: tail) tail') x₀
addCoeffs.hmonomCoeff R G x₀ (a₁ * b, x * h) + (monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀ = monomCoeff R G x₀ (a₁ * b, x * h) + monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀ + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x: G
tail: FormalSum R G
x₀: G
rel':= addCoeffs a₁ a₂ x tail: ElementaryMove R G ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail)
prev:= first_arg_invariant ((a₁, x) :: (a₂, x) :: tail) ((a₁ + a₂, x) :: tail) tail' rel': mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈ mul ((a₁ + a₂, x) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x) :: (a₂, x) :: tail) tail') x₀ = coords (mul ((a₁ + a₂, x) :: tail) tail') x₀
addCoeffs.hmonomCoeff R G x₀ (a₁ * b, x * h) + (monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀ = monomCoeff R G x₀ (a₁ * b, x * h) + monomCoeff R G x₀ (a₂ * b, x * h) + coords (mulMonom b h tail) x₀ + coords (mul ((a₁ + a₂, x) :: tail) tail') x₀Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: GElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: G
aElementaryMove R G s₁ s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: GElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: G
rel':= cons a x s₁ s₂ r: ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)
prev:= first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel': mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail'
cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: G
rel':= cons a x s₁ s₂ r: ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)
prev:= first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel': mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail'
pl:= congrFun prev x₀: coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀
cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: G
rel':= cons a x s₁ s₂ r: ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)
prev:= first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel': mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail'
pl:= congrFun prev x₀: coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀
cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: G
rel':= cons a x s₁ s₂ r: ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)
prev:= first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel': mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail'
pl:= congrFun prev x₀: coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀
cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: G
rel':= cons a x s₁ s₂ r: ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)
prev:= first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel': mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail'
pl:= congrFun prev x₀: coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀
cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: G
rel':= cons a x s₁ s₂ r: ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)
prev:= first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel': mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail'
pl:= congrFun prev x₀: coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀
ps:= mul_monom_invariant b h x₀ s₁ s₂ r: coords (mulMonom b h s₁) x₀ = coords (mulMonom b h s₂) x₀
cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: G
rel':= cons a x s₁ s₂ r: ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)
prev:= first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel': mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail'
pl:= congrFun prev x₀: coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀
ps:= mul_monom_invariant b h x₀ s₁ s₂ r: coords (mulMonom b h s₁) x₀ = coords (mulMonom b h s₂) x₀
cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁✝, s₂✝: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a: R
x: G
s₁, s₂: FormalSum R G
r: ElementaryMove R G s₁ s₂
a_ih✝: mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀: G
rel':= cons a x s₁ s₂ r: ElementaryMove R G ((a, x) :: s₁) ((a, x) :: s₂)
prev:= first_arg_invariant ((a, x) :: s₁) ((a, x) :: s₂) tail' rel': mul ((a, x) :: s₁) tail' ≈ mul ((a, x) :: s₂) tail'
pl:= congrFun prev x₀: coords (mul ((a, x) :: s₁) tail') x₀ = coords (mul ((a, x) :: s₂) tail') x₀
ps:= mul_monom_invariant b h x₀ s₁ s₂ r: coords (mulMonom b h s₁) x₀ = coords (mulMonom b h s₂) x₀
cons.hGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords ((a₁ * b, x₁ * h) :: mulMonom b h tail) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords ((a₁ * b, x₁ * h) :: mulMonom b h tail) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords ((a₁ * b, x₁ * h) :: mulMonom b h tail) x₀ + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀ = monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀) + coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) = monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀
swap.hmonomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) = monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀monomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀monomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h) = monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀monomCoeff R G x₀ (a₁ * b, x₁ * h) + monomCoeff R G x₀ (a₂ * b, x₂ * h)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)/-- multiplication for free modules -/ def mul :R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
s₁, s₂: FormalSum R G
head': R × G
tail': List (R × G)
b: R
h: G
a₁, a₂: R
x₁, x₂: G
tail: FormalSum R G
x₀: G
rel':= swap a₁ a₂ x₁ x₂ tail: ElementaryMove R G ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)
prev:= first_arg_invariant ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) tail' rel': mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail' ≈ mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail'
pl:= congrFun prev x₀: coords (mul ((a₁, x₁) :: (a₂, x₂) :: tail) tail') x₀ = coords (mul ((a₂, x₂) :: (a₁, x₁) :: tail) tail') x₀monomCoeff R G x₀ (a₂ * b, x₂ * h) + monomCoeff R G x₀ (a₁ * b, x₁ * h)R[R: TypeG] →G: TypeR[R: TypeG] →G: TypeR[R: TypeG] :=G: TypeR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
a∀ (s₁ s₂ : FormalSum R G), ElementaryMove R G s₁ s₂ → f s₁ = f s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
af s₁ = f s₂R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
a.h.a∀ (a : FormalSum R G), mulAux s₁ (Quotient.mk (formalSumSetoid R G) a) = mulAux s₂ (Quotient.mk (formalSumSetoid R G) a)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
a.h.amulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
a.h.amulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R GmulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
lhs:= Eq.refl (mulAux s₁ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)
a.h.amulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
lhs:= Eq.refl (mulAux s₁ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)mulAux s₂ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
lhs:= Eq.refl (mulAux s₁ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)
rhs:= Eq.refl (mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₂ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)
a.h.amulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
lhs:= Eq.refl (mulAux s₁ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)
rhs:= Eq.refl (mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₂ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)
a.h.aQuotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t) = mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
lhs:= Eq.refl (mulAux s₁ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)
rhs:= Eq.refl (mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₂ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)
a.h.amulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
lhs:= Eq.refl (mulAux s₁ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)
rhs:= Eq.refl (mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₂ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)
a.h.aQuotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
lhs:= Eq.refl (mulAux s₁ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)
rhs:= Eq.refl (mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₂ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)
a.h.aQuotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
lhs:= Eq.refl (mulAux s₁ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)
rhs:= Eq.refl (mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₂ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)
a.h.aFormalSum.mul s₁ t ≈ FormalSum.mul s₂ tR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
f:= fun s t => mulAux s t: FormalSum R G → R[G] → R[G]
s₁, s₂: FormalSum R G
rel: ElementaryMove R G s₁ s₂
t: FormalSum R G
lhs:= Eq.refl (mulAux s₁ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₁ t)
rhs:= Eq.refl (mulAux s₂ (Quotient.mk (formalSumSetoid R G) t)): mulAux s₂ (Quotient.mk (formalSumSetoid R G) t) = Quotient.mk (formalSumSetoid R G) (FormalSum.mul s₂ t)
a.h.a.relElementaryMove R G s₁ s₂/-! ## The Ring Structure -/ instance groupRingMul : Mul (Goals accomplished! 🐙R[R: TypeG]) := ⟨mul⟩G: Typeinstance : One (R[R: TypeG]) := ⟨⟦[(G: Type1,1: ?m.449181)]⟧⟩1: ?m.44951instance : AddCommGroup (instance: {R : Type} → [inst : Ring R] → {G : Type} → [inst_1 : DecidableEq G] → AddCommGroup (R[G])R[R: TypeG]) := { zero := ⟦G: Type[] ⟧ add := FreeModule.add add_assoc := FreeModule.addn_assoc add_zero := FreeModule.addn_zero zero_add := FreeModule.zero_addn add_comm := FreeModule.addn_comm add_left_neg :=[]: List ?m.45566R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: R[G]
l: -1 • x + x = Quotient.mk (formalSumSetoid R G) []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: R[G]
l: -1 • x + x = Quotient.mk (formalSumSetoid R G) []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: R[G]
l: -1 • x + x = Quotient.mk (formalSumSetoid R G) []} /-- The group ring is a ring -/Goals accomplished! 🐙instance : Ring (instance: {R : Type} → [inst : Ring R] → [inst_1 : DecidableEq R] → {G : Type} → [inst_2 : Group G] → [inst_3 : DecidableEq G] → Ring (R[G])R[R: TypeG]) := { mul := mul neg := funG: Typex => (-x: ?m.475421 :1: ?m.47555R) •R: Typex sub_eq_add_neg :=x: ?m.47542add_left_neg :=Goals accomplished! 🐙Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: R[G]
l: -1 • x + x = Quotient.mk (formalSumSetoid R G) []
lc: -1 + 1 = 0R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: R[G]
l: -1 • x + x = Quotient.mk (formalSumSetoid R G) []
lc: -1 + 1 = 0R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: R[G]
l: -1 • x + x = Quotient.mk (formalSumSetoid R G) []
lc: -1 + 1 = 0left_distrib :=Goals accomplished! 🐙∀ (a : FormalSum R G) (b c : R[G]), Quotient.mk (formalSumSetoid R G) a * (b + c) = Quotient.mk (formalSumSetoid R G) a * b + Quotient.mk (formalSumSetoid R G) a * cR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G∀ (b c : R[G]), Quotient.mk (formalSumSetoid R G) x * (b + c) = Quotient.mk (formalSumSetoid R G) x * b + Quotient.mk (formalSumSetoid R G) x * cR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G∀ (a b : FormalSum R G), Quotient.mk (formalSumSetoid R G) x * (Quotient.mk (formalSumSetoid R G) a + Quotient.mk (formalSumSetoid R G) b) = Quotient.mk (formalSumSetoid R G) x * Quotient.mk (formalSumSetoid R G) a + Quotient.mk (formalSumSetoid R G) x * Quotient.mk (formalSumSetoid R G) bR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R GQuotient.mk (formalSumSetoid R G) x * (Quotient.mk (formalSumSetoid R G) y + Quotient.mk (formalSumSetoid R G) z) = Quotient.mk (formalSumSetoid R G) x * Quotient.mk (formalSumSetoid R G) y + Quotient.mk (formalSumSetoid R G) x * Quotient.mk (formalSumSetoid R G) zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
aFormalSum.mul x (y ++ z) ≈ FormalSum.mul x y ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
aFormalSum.mul x (y ++ z) ≈ FormalSum.mul x y ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
a.nilFormalSum.mul x ([] ++ z) ≈ FormalSum.mul x [] ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
a.nilFormalSum.mul x z ≈ FormalSum.mul x [] ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
a.nilFormalSum.mul x ([] ++ z) ≈ FormalSum.mul x [] ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
a.nilFormalSum.mul x z ≈ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
a.nilFormalSum.mul x ([] ++ z) ≈ FormalSum.mul x [] ++ FormalSum.mul x zGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
aFormalSum.mul x (y ++ z) ≈ FormalSum.mul x y ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.consFormalSum.mul x (h :: t ++ z) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.consmulMonom h.fst h.snd x ++ FormalSum.mul x (t ++ z) ≈ mulMonom h.fst h.snd x ++ (FormalSum.mul x t ++ FormalSum.mul x z)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.consFormalSum.mul x (h :: t ++ z) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.cons.h∀ (x_1 : G), coords (mulMonom h.fst h.snd x ++ FormalSum.mul x (t ++ z)) x_1 = coords (mulMonom h.fst h.snd x ++ (FormalSum.mul x t ++ FormalSum.mul x z)) x_1R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.cons.h∀ (x_1 : G), coords (mulMonom h.fst h.snd x ++ FormalSum.mul x (t ++ z)) x_1 = coords (mulMonom h.fst h.snd x ++ (FormalSum.mul x t ++ FormalSum.mul x z)) x_1R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.consFormalSum.mul x (h :: t ++ z) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
a.cons.hcoords (mulMonom h.fst h.snd x ++ FormalSum.mul x (t ++ z)) x₀ = coords (mulMonom h.fst h.snd x ++ (FormalSum.mul x t ++ FormalSum.mul x z)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.consFormalSum.mul x (h :: t ++ z) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
a.cons.hcoords (mulMonom h.fst h.snd x ++ FormalSum.mul x (t ++ z)) x₀ = coords (mulMonom h.fst h.snd x ++ (FormalSum.mul x t ++ FormalSum.mul x z)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
a.cons.hcoords (mulMonom h.fst h.snd x) x₀ + coords (FormalSum.mul x (t ++ z)) x₀ = coords (mulMonom h.fst h.snd x ++ (FormalSum.mul x t ++ FormalSum.mul x z)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
a.cons.hcoords (mulMonom h.fst h.snd x) x₀ + coords (FormalSum.mul x (t ++ z)) x₀ = coords (mulMonom h.fst h.snd x ++ (FormalSum.mul x t ++ FormalSum.mul x z)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
a.cons.hcoords (mulMonom h.fst h.snd x) x₀ + coords (FormalSum.mul x (t ++ z)) x₀ = coords (mulMonom h.fst h.snd x) x₀ + (coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
a.cons.hcoords (mulMonom h.fst h.snd x) x₀ + coords (FormalSum.mul x (t ++ z)) x₀ = coords (mulMonom h.fst h.snd x) x₀ + coords (FormalSum.mul x t ++ FormalSum.mul x z) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
a.cons.hcoords (mulMonom h.fst h.snd x) x₀ + coords (FormalSum.mul x (t ++ z)) x₀ = coords (mulMonom h.fst h.snd x) x₀ + coords (FormalSum.mul x t ++ FormalSum.mul x z) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.consFormalSum.mul x (h :: t ++ z) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
a.cons.hcoords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.consFormalSum.mul x (h :: t ++ z) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
lih:= congrFun ih x₀: coords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t ++ FormalSum.mul x z) x₀
a.cons.hcoords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.consFormalSum.mul x (h :: t ++ z) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
lih:= congrFun ih x₀: coords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t ++ FormalSum.mul x z) x₀
a.cons.hcoords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
lih: coords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀
a.cons.hcoords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
lih: coords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀
a.cons.hcoords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
lih: coords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀
a.cons.hcoords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
a.consFormalSum.mul x (h :: t ++ z) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul x zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
lih: coords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀
a.cons.hcoords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, z: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul x (t ++ z) ≈ FormalSum.mul x t ++ FormalSum.mul x z
x₀: G
lih: coords (FormalSum.mul x (t ++ z)) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀
a.cons.hcoords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul x z) x₀right_distrib :=Goals accomplished! 🐙∀ (a : FormalSum R G) (b c : R[G]), (Quotient.mk (formalSumSetoid R G) a + b) * c = Quotient.mk (formalSumSetoid R G) a * c + b * cR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G∀ (b c : R[G]), (Quotient.mk (formalSumSetoid R G) x + b) * c = Quotient.mk (formalSumSetoid R G) x * c + b * cR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G∀ (a b : FormalSum R G), (Quotient.mk (formalSumSetoid R G) x + Quotient.mk (formalSumSetoid R G) a) * Quotient.mk (formalSumSetoid R G) b = Quotient.mk (formalSumSetoid R G) x * Quotient.mk (formalSumSetoid R G) b + Quotient.mk (formalSumSetoid R G) a * Quotient.mk (formalSumSetoid R G) bR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G(Quotient.mk (formalSumSetoid R G) x + Quotient.mk (formalSumSetoid R G) y) * Quotient.mk (formalSumSetoid R G) z = Quotient.mk (formalSumSetoid R G) x * Quotient.mk (formalSumSetoid R G) z + Quotient.mk (formalSumSetoid R G) y * Quotient.mk (formalSumSetoid R G) zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
aFormalSum.mul (x ++ y) z ≈ FormalSum.mul x z ++ FormalSum.mul y zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
aFormalSum.mul (x ++ y) z ≈ FormalSum.mul x z ++ FormalSum.mul y zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
a.nilFormalSum.mul (x ++ y) [] ≈ FormalSum.mul x [] ++ FormalSum.mul y []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
a.nil[] ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
a.nilFormalSum.mul (x ++ y) [] ≈ FormalSum.mul x [] ++ FormalSum.mul y []Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
aFormalSum.mul (x ++ y) z ≈ FormalSum.mul x z ++ FormalSum.mul y zR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h: G
a.consFormalSum.mul (x ++ y) ((a, h) :: t) ≈ FormalSum.mul x ((a, h) :: t) ++ FormalSum.mul y ((a, h) :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h: G
a.consmulMonom a h (x ++ y) ++ FormalSum.mul (x ++ y) t ≈ mulMonom a h x ++ (FormalSum.mul x t ++ (mulMonom a h y ++ FormalSum.mul y t))R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
a.cons.hcoords (mulMonom a h (x ++ y) ++ FormalSum.mul (x ++ y) t) x₀ = coords (mulMonom a h x ++ (FormalSum.mul x t ++ (mulMonom a h y ++ FormalSum.mul y t))) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
a.cons.hcoords (mulMonom a h (x ++ y) ++ FormalSum.mul (x ++ y) t) x₀ = coords (mulMonom a h x ++ (FormalSum.mul x t ++ (mulMonom a h y ++ FormalSum.mul y t))) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih:= congrFun ih x₀: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t ++ FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih:= congrFun ih x₀: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t ++ FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h✝: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a: R
h, x₀: G
lih: coords (FormalSum.mul (x ++ y) t) x₀ = coords (FormalSum.mul x t) x₀ + coords (FormalSum.mul y t) x₀
a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
h: R × G
t: List (R × G)
ih: FormalSum.mul (x ++ y) t ≈ FormalSum.mul x t ++ FormalSum.mul y t
a.consFormalSum.mul (x ++ y) (h :: t) ≈ FormalSum.mul x (h :: t) ++ FormalSum.mul y (h :: t)zero_mul :=Goals accomplished! 🐙
a∀ (a : FormalSum R G), 0 * Quotient.mk (formalSumSetoid R G) a = 0R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a0 * Quotient.mk (formalSumSetoid R G) x = 0R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a.aFormalSum.mul [] x ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a.aFormalSum.mul [] x ≈ []
a.a.nilFormalSum.mul [] [] ≈ []Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a.aFormalSum.mul [] x ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consmulMonom h.fst h.snd [] ++ FormalSum.mul [] t ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consmulMonom h.fst h.snd [] ++ FormalSum.mul [] t ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consmulMonom h.fst h.snd [] ++ FormalSum.mul [] t ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih:= congrFun ih x₀: coords (FormalSum.mul [] t) x₀ = coords [] x₀
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih:= congrFun ih x₀: coords (FormalSum.mul [] t) x₀ = coords [] x₀
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
a.a.consFormalSum.mul [] (h :: t) ≈ []R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
h: R × G
t: List (R × G)
ih: FormalSum.mul [] t ≈ []
x₀: G
lih: coords (FormalSum.mul [] t) x₀ = 0
a.a.cons.hmul_zero :=Goals accomplished! 🐙
a∀ (a : FormalSum R G), Quotient.mk (formalSumSetoid R G) a * 0 = 0R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
aQuotient.mk (formalSumSetoid R G) x * 0 = 0one := ⟦[(Goals accomplished! 🐙1,1: ?m.473311)]⟧ natCast := fun1: ?m.47361n => ⟦ [(n: ?m.47470n,n: ?m.474701)] ⟧ natCast_zero :=1: ?m.47527NatCast.natCast 0 = 0
a[(↑0, 1)] ≈ []NatCast.natCast 0 = 0
a.h
a.hNatCast.natCast 0 = 0
a.hNatCast.natCast 0 = 0NatCast.natCast 0 = 0natCast_succ :=Goals accomplished! 🐙∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1NatCast.natCast (n + 1) = NatCast.natCast n + 1∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
a∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1Goals accomplished! 🐙mul_assoc :=Goals accomplished! 🐙∀ (a : FormalSum R G) (b c : R[G]), Quotient.mk (formalSumSetoid R G) a * b * c = Quotient.mk (formalSumSetoid R G) a * (b * c)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G∀ (b c : R[G]), Quotient.mk (formalSumSetoid R G) x * b * c = Quotient.mk (formalSumSetoid R G) x * (b * c)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G∀ (a b : FormalSum R G), Quotient.mk (formalSumSetoid R G) x * Quotient.mk (formalSumSetoid R G) a * Quotient.mk (formalSumSetoid R G) b = Quotient.mk (formalSumSetoid R G) x * (Quotient.mk (formalSumSetoid R G) a * Quotient.mk (formalSumSetoid R G) b)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R GQuotient.mk (formalSumSetoid R G) x * Quotient.mk (formalSumSetoid R G) y * Quotient.mk (formalSumSetoid R G) z = Quotient.mk (formalSumSetoid R G) x * (Quotient.mk (formalSumSetoid R G) y * Quotient.mk (formalSumSetoid R G) z)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
aFormalSum.mul (FormalSum.mul x y) z ≈ FormalSum.mul x (FormalSum.mul y z)R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
a.h∀ (x_1 : G), coords (FormalSum.mul (FormalSum.mul x y) z) x_1 = coords (FormalSum.mul x (FormalSum.mul y z)) x_1R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
a.h∀ (x_1 : G), coords (FormalSum.mul (FormalSum.mul x y) z) x_1 = coords (FormalSum.mul x (FormalSum.mul y z)) x_1R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
x₀: G
a.hcoords (FormalSum.mul (FormalSum.mul x y) z) x₀ = coords (FormalSum.mul x (FormalSum.mul y z)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
x₀: G
a.hcoords (FormalSum.mul (FormalSum.mul x y) z) x₀ = coords (FormalSum.mul x (FormalSum.mul y z)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
x₀: G
a.hcoords (FormalSum.mul (FormalSum.mul x y) z) x₀ = coords (FormalSum.mul x (FormalSum.mul y z)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
a.h.nilcoords (FormalSum.mul (FormalSum.mul x y) []) x₀ = coords (FormalSum.mul x (FormalSum.mul y [])) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
a.h.nilcoords (FormalSum.mul (FormalSum.mul x y) []) x₀ = coords (FormalSum.mul x (FormalSum.mul y [])) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
a.h.nilcoords (FormalSum.mul (FormalSum.mul x y) []) x₀ = coords (FormalSum.mul x (FormalSum.mul y [])) x₀Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y, z: FormalSum R G
x₀: G
a.hcoords (FormalSum.mul (FormalSum.mul x y) z) x₀ = coords (FormalSum.mul x (FormalSum.mul y z)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a.h.conscoords (FormalSum.mul (FormalSum.mul x y) (h :: t)) x₀ = coords (FormalSum.mul x (FormalSum.mul y (h :: t))) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (FormalSum.mul (FormalSum.mul x y) ((a, h) :: t)) x₀ = coords (FormalSum.mul x (FormalSum.mul y ((a, h) :: t))) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a.h.conscoords (FormalSum.mul (FormalSum.mul x y) (h :: t)) x₀ = coords (FormalSum.mul x (FormalSum.mul y (h :: t))) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y) ++ FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y ++ FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a.h.conscoords (FormalSum.mul (FormalSum.mul x y) (h :: t)) x₀ = coords (FormalSum.mul x (FormalSum.mul y (h :: t))) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y) ++ FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y ++ FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y) ++ FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y ++ FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y ++ FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y ++ FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y ++ FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y ++ FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a.h.conscoords (FormalSum.mul (FormalSum.mul x y) (h :: t)) x₀ = coords (FormalSum.mul x (FormalSum.mul y (h :: t))) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y ++ FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a.h.conscoords (FormalSum.mul (FormalSum.mul x y) (h :: t)) x₀ = coords (FormalSum.mul x (FormalSum.mul y (h :: t))) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (mulMonom a h y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀ = coords (FormalSum.mul x (mulMonom a h y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀ = coords (FormalSum.mul x (mulMonom a h y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a.h.conscoords (FormalSum.mul (FormalSum.mul x y) (h :: t)) x₀ = coords (FormalSum.mul x (FormalSum.mul y (h :: t))) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (mulMonom a h (FormalSum.mul x y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀ = coords (FormalSum.mul x (mulMonom a h y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x, y: FormalSum R G
x₀: G
h✝: R × G
t: List (R × G)
ih: coords (FormalSum.mul (FormalSum.mul x y) t) x₀ = coords (FormalSum.mul x (FormalSum.mul y t)) x₀
a: R
h: G
a.h.conscoords (FormalSum.mul x (mulMonom a h y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀ = coords (FormalSum.mul x (mulMonom a h y)) x₀ + coords (FormalSum.mul x (FormalSum.mul y t)) x₀mul_one :=Goals accomplished! 🐙
a∀ (a : FormalSum R G), Quotient.mk (formalSumSetoid R G) a * 1 = Quotient.mk (formalSumSetoid R G) aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
aQuotient.mk (formalSumSetoid R G) x * 1 = Quotient.mk (formalSumSetoid R G) xR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a.aFormalSum.mul x [(1, 1)] ≈ xR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a.a.h∀ (x_1 : G), coords (FormalSum.mul x [(1, 1)]) x_1 = coords x x_1R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a.a.h∀ (x_1 : G), coords (FormalSum.mul x [(1, 1)]) x_1 = coords x x_1R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
x₀: G
a.a.hcoords (FormalSum.mul x [(1, 1)]) x₀ = coords x x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
x₀: G
a.a.hcoords (FormalSum.mul x [(1, 1)]) x₀ = coords x x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
x₀: G
a.a.hcoords (FormalSum.mul x [(1, 1)]) x₀ = coords x x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
x₀: G
a.a.hcoords (FormalSum.mul x [(1, 1)]) x₀ = coords x x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
x₀: G
a.a.hR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
x₀: G
a.a.h
a.a.h.nilGoals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (mulMonom 1 1 t) x₀ = coords t x₀
a: R
x: G
m: (x == x₀) = false
a.a.h.cons.falseR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (mulMonom 1 1 t) x₀ = coords t x₀
a: R
x: G
m: (x == x₀) = true
a.a.h.cons.trueR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (mulMonom 1 1 t) x₀ = coords t x₀
a: R
x: G
m: (x == x₀) = false
a.a.h.cons.falseR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (mulMonom 1 1 t) x₀ = coords t x₀
a: R
x: G
m: (x == x₀) = true
a.a.h.cons.trueone_mul :=Goals accomplished! 🐙
a∀ (a : FormalSum R G), 1 * Quotient.mk (formalSumSetoid R G) a = Quotient.mk (formalSumSetoid R G) aR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a1 * Quotient.mk (formalSumSetoid R G) x = Quotient.mk (formalSumSetoid R G) xR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a.aFormalSum.mul [(1, 1)] x ≈ xR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a.a.h∀ (x_1 : G), coords (FormalSum.mul [(1, 1)] x) x_1 = coords x x_1R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
a.a.h∀ (x_1 : G), coords (FormalSum.mul [(1, 1)] x) x_1 = coords x x_1R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
x₀: G
a.a.hcoords (FormalSum.mul [(1, 1)] x) x₀ = coords x x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
x₀: G
a.a.hcoords (FormalSum.mul [(1, 1)] x) x₀ = coords x x₀
a.a.h.nilcoords (FormalSum.mul [(1, 1)] []) x₀ = coords [] x₀Goals accomplished! 🐙R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x: FormalSum R G
x₀: G
a.a.hcoords (FormalSum.mul [(1, 1)] x) x₀ = coords x x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a.a.h.consR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.consR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a.a.h.consR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.consR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (FormalSum.mul [(1, 1)] ((a, x) :: t)) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.consR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (FormalSum.mul [(1, 1)] ((a, x) :: t)) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (FormalSum.mul [(1, 1)] ((a, x) :: t)) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (FormalSum.mul [(1, 1)] ((a, x) :: t)) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a.a.h.consR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (FormalSum.mul [(1, 1)] ((a, x) :: t)) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a.a.h.consR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (FormalSum.mul [(1, 1)] ((a, x) :: t)) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (mulMonom a x [(1, 1)] ++ FormalSum.mul [(1, 1)] t) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (mulMonom a x [(1, 1)] ++ FormalSum.mul [(1, 1)] t) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a.a.h.consR: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (mulMonom a x [(1, 1)] ++ FormalSum.mul [(1, 1)] t) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (mulMonom a x [(1, 1)]) x₀ + coords (FormalSum.mul [(1, 1)] t) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a: R
x: G
a.a.h.conscoords (mulMonom a x [(1, 1)]) x₀ + coords (FormalSum.mul [(1, 1)] t) x₀ = monomCoeff R G x₀ (a, x) + coords t x₀R: Type
inst✝³: Ring R
inst✝²: DecidableEq R
G: Type
inst✝¹: Group G
inst✝: DecidableEq G
x₀: G
h: R × G
t: List (R × G)
ih: coords (FormalSum.mul [(1, 1)] t) x₀ = coords t x₀
a.a.h.cons} end GroupRingGoals accomplished! 🐙