@[instance_reducible]

def HexPolyMathlib.commRingOfGrind {R : Type u} [s : Lean.Grind.CommRing R] : CommRing R

Mathlib's CommRing structure on a type carrying Lean.Grind.CommRing, with every operation taken from that instance.

Equations

• One or more equations did not get rendered due to their size.

theorem HexPolyMathlib.toGrind_commRingOfGrind {R : Type u} [s : Lean.Grind.CommRing R] : CommRing.toGrindCommRing R = s

The Lean.Grind.CommRing reduct of commRingOfGrind is the instance it was built from. Rewriting with this equation moves a Mathlib-side theorem stated over [CommRing R] onto a goal stated over the executable instance.

class HexPolyMathlib.GrindReduct (R : Type u) [s : Lean.Grind.CommRing R] [inst : CommRing R] : Prop

A Mathlib CommRing structure whose Lean.Grind.CommRing reduct is the carrier's executable instance. A bridge theorem stated over [CommRing R] can be moved onto a goal stated over the executable instance exactly when this holds.

The default proof discharges the field-by-field comparison: every field is a projection of the same instance except the numerals, which agree by Lean.Grind.Semiring.ofNat_eq_natCast.

• toGrind_eq : CommRing.toGrindCommRing R = s

  The Mathlib structure reduces to the executable instance.

instance HexPolyMathlib.instGrindReductOfGrind {R : Type u} [s : Lean.Grind.CommRing R] : GrindReduct R

@[instance_reducible]

def HexPolyMathlib.denseCommRing {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] : CommRing (Hex.DensePoly R)

Mathlib's CommRing structure on the executable dense polynomials, with the executable operations. This covers Hex.ZPoly and the executable finite-field polynomials, which are Hex.DensePoly at Int and at Hex.ZMod64 p.

Equations

• HexPolyMathlib.denseCommRing = HexPolyMathlib.commRingOfGrind