English
There are several equivalent ways to say that a number z is real.
Русский
Существует несколько эквивалентных формулировок того, что число z реально.
LaTeX
$$$\text{IsReal}(z) \;\Leftrightarrow\; \text{Conj}(z) = z \;\text{в рамках множества условий}$$$
Lean4
/-- There are several equivalent ways to say that a number `z` is in fact a real number. -/
theorem is_real_TFAE (z : K) : TFAE [conj z = z, ∃ r : ℝ, (r : K) = z, ↑(re z) = z, im z = 0, IsSelfAdjoint z] :=
by
tfae_have 1 → 4
| h => by rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div, ofReal_zero]
tfae_have 4 → 3
| h => by conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
tfae_have 3 → 2 := fun h => ⟨_, h⟩
tfae_have 2 → 1 := fun ⟨r, hr⟩ => hr ▸ conj_ofReal _
tfae_have 1 → 5 := fun _ => by rwa [isSelfAdjoint_iff]
tfae_have 5 → 1 := fun hz => by rwa [isSelfAdjoint_iff] at hz
tfae_finish
