choose_zero_ite — Mathlib

English

The value of choose 0 k is 1 if k = 0 and 0 otherwise.

Русский

Значение choose 0 k равно 1, если k = 0, и 0 в противном случае.

LaTeX

$$$ \forall k\in\mathbb{N},\ choose\ 0\ k = \begin{cases}1,& k=0 \\ 0,& k>0\end{cases}$$$

Lean4

theorem choose_zero_ite (R) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (k : ℕ) :
    choose (0 : R) k = if k = 0 then 1 else 0 := by
  split_ifs with hk
  · rw [hk, choose_zero_right]
  · rw [choose_zero_pos R <| Nat.pos_of_ne_zero hk]

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