ringEquivCongr_ringEquivCongr_apply

English

Given hab: a=b and hbc: b=c, and x ∈ ZMod a, ringEquivCongr hbc (ringEquivCongr hab x) = ringEquivCongr (hab.trans hbc) x.

Русский

Пусть hab: a=b, hbc: b=c, и x ∈ ZMod a. Тогда ringEquivCongr hbc (ringEquivCongr hab x) = ringEquivCongr (hab.trans hbc) x.

LaTeX

$$$ ringEquivCongr hbc (ringEquivCongr hab x) = ringEquivCongr (hab.trans hbc) x $$$

Lean4

theorem ringEquivCongr_ringEquivCongr_apply {a b c : ℕ} (hab : a = b) (hbc : b = c) (x : ZMod a) :
    ringEquivCongr hbc (ringEquivCongr hab x) = ringEquivCongr (hab.trans hbc) x :=
  by
  rw [← ringEquivCongr_trans hab hbc]
  rfl

Похожие утверждения