nf_opow — Mathlib

English

If o1 and o2 are ONote in normal form, then their exponentiation o1^o2 is in normal form: NF(o1^o2).

Русский

Если o1 и o2 — ONote в нормальной форме, тогда возведение в степень o1^o2 находится в нормальной форме: NF(o1^o2).

LaTeX

$$$\\forall o_1\\,o_2:\\,[NF\\ o_1]\\,[NF\\ o_2]\\;\\Rightarrow \\operatorname{NF}(o_1^{o_2})$$$

Lean4

instance nf_opow (o₁ o₂) [NF o₁] [NF o₂] : NF (o₁ ^ o₂) :=
  by
  rcases e₁ : split o₁ with ⟨a, m⟩
  have na := (nf_repr_split e₁).1
  rcases e₂ : split' o₂ with ⟨b', k⟩
  haveI := (nf_repr_split' e₂).1
  obtain - | ⟨a0, n, a'⟩ := a
  · rcases m with - | m
    · by_cases o₂ = 0 <;> simp only [(· ^ ·), Pow.pow, opow, opowAux2, *] <;> decide
    · by_cases m = 0
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, *, zero_def]
        decide
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, *]
        infer_instance
  · simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, split_eq_scale_split' e₂, mulNat_eq_mul]
    have := na.fst
    rcases k with - | k
    · infer_instance
    · cases k <;> cases m <;> infer_instance

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