pos_invOf_of_invertible_cast — Mathlib

English

Theorem pos_invOf_of_invertible_cast asserts that the inverse of a positive natural cast is positive.

Русский

Теорема pos_invOf_of_invertible_cast утверждает, что обратное положительно при положительном образе натурального числа.

LaTeX

$$$ 0 < ⅟(n : R) \quad \text{for } n > 0 \text{ and invertible }(n:R)$$$

Lean4

theorem pos_invOf_of_invertible_cast [Nontrivial R] (n : ℕ) [Invertible (n : R)] : 0 < ⅟(n : R) :=
  invOf_pos.2 <| Nat.cast_pos.2 <| pos_of_invertible_cast (R := R) n

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