compatibleRingOfRingStructure — Mathlib

Lean4
/-- Given a Type `R` with a `Language.ring.Structure R`, the instance given by
`addOfRingStructure` etc. are compatible with the `Language.ring.Structure` instance on `R`.

This definition is only to be used when `addOfRingStructure`, `mulOfRingStructure` etc
are local instances.
-/
abbrev compatibleRingOfRingStructure : CompatibleRing R :=
  { funMap_add := by
      simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
      intros; rfl
    funMap_mul := by
      simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
      intros; rfl
    funMap_neg := by
      simp only [Fin.forall_fin_succ_pi, Fin.cons_zero, Fin.forall_fin_zero_pi]
      intros; rfl
    funMap_zero := by
      simp only [Fin.forall_fin_zero_pi]
      rfl
    funMap_one := by
      simp only [Fin.forall_fin_zero_pi]
      rfl }
Похожие утверждения