English
From any semiring α one obtains a GrindSemiring structure on α that is compatible with the semiring operations.
Русский
Для любого полусемиринга α существует совместная структура GrindSemiring на α, совместимая с операциями полусемиринга.
LaTeX
$$$$ \exists s:\text{GrindSemiring}(\alpha). $$$$
Lean4
instance (priority := 100) toGrindSemiring [s : Semiring α] : Grind.Semiring α :=
{ s with
nsmul := ⟨s.nsmul⟩
npow := ⟨fun a n => a ^ n⟩
ofNat
| 0 | 1 | n + 2 => inferInstance
natCast := inferInstance
add_zero := by simp [add_zero]
mul_one := by simp [mul_one]
zero_mul := by simp [zero_mul]
pow_zero a := by simp
pow_succ a n := by simp [pow_succ]
ofNat_eq_natCast
| 0 => Nat.cast_zero.symm
| 1 => Nat.cast_one.symm
| n + 2 => rfl
ofNat_succ
| 0 => by simp [zero_add]
| 1 => by
change Nat.cast 2 = 1 + 1
rw [one_add_one_eq_two]
rfl
| n + 2 => by
change Nat.cast (n + 2 + 1) = Nat.cast (n + 2) + 1
rw [← AddMonoidWithOne.natCast_succ]
nsmul_eq_natCast_mul n a := nsmul_eq_mul n a }
