repr_mul — Mathlib

English

For NF factors o1 and o2, the representation of their product equals the product of representations: repr(o1 * o2) = repr(o1) · repr(o2).

Русский

Для NF-образующихся факторoв o1 и o2 выполняется равенство repr(o1 * o2) = repr(o1) · repr(o2).

LaTeX

$$$\forall o_1\, o_2\ [o_1\NF] [o_2\NF],\; \mathrm{repr}(o_1 * o_2) = \mathrm{repr}(o_1) \cdot \mathrm{repr}(o_2).$$$

Lean4

@[simp]
theorem repr_mul : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ * o₂) = repr o₁ * repr o₂
  | 0, o, _, h₂ => by cases o <;> exact (zero_mul _).symm
  | oadd _ _ _, 0, _, _ => (mul_zero _).symm
  | oadd e₁ n₁ a₁, oadd e₂ n₂ a₂, h₁, h₂ =>
    by
    have IH : repr (mul _ _) = _ := @repr_mul _ _ h₁ h₂.snd
    conv =>
      lhs
      simp [(· * ·)]
    have ao : repr a₁ + ω ^ repr e₁ * (n₁ : ℕ) = ω ^ repr e₁ * (n₁ : ℕ) :=
      by
      apply add_absorp h₁.snd'.repr_lt
      simpa using (mul_le_mul_iff_right₀ <| opow_pos _ omega0_pos).2 (Nat.cast_le.2 n₁.2)
    by_cases e0 : e₂ = 0
    · obtain ⟨x, xe⟩ := Nat.exists_eq_succ_of_ne_zero n₂.ne_zero
      simp only [Mul.mul, mul, e0, ↓reduceIte, repr, PNat.mul_coe, natCast_mul, opow_zero, one_mul]
      simp only [xe, h₂.zero_of_zero e0, repr, add_zero]
      rw [natCast_succ x, add_mul_succ _ ao, mul_assoc]
    · simp only [repr]
      haveI := h₁.fst
      haveI := h₂.fst
      simp only [Mul.mul, mul, e0, ite_false, repr.eq_2, repr_add, opow_add, IH, repr, mul_add]
      rw [← mul_assoc]
      congr 2
      have := mt repr_inj.1 e0
      rw [add_mul_of_isSuccLimit ao (isSuccLimit_opow_left isSuccLimit_omega0 this), mul_assoc,
        mul_omega0_dvd (Nat.cast_pos'.2 n₁.pos) (nat_lt_omega0 _)]
      simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 this)

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