`BookProof.ChapterEulerStochastic.preservesProb_iff_exists_angles` (M : Matrix (Fin 2) (Fin 2) ℝ) : PreservesProb M ↔ ∃ a b : ℝ, M = Mmat a b

Proved

BookProof.ChapterEulerStochastic.preservesProb_iff_exists_angles

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterEulerStochastic.

BookProof.ChapterEulerStochastic.preservesProb_iff_exists_angles (M : Matrix (Fin 2) (Fin 2) ℝ) : PreservesProb M ↔ ∃ a b : ℝ, M = Mmat a b

Formalization note: Lean 4 identifier BookProof.ChapterEulerStochastic.preservesProb_iff_exists_angles.

Preamble

-- Generated from ChapterEulerStochastic.lean — theorem BookProof.ChapterEulerStochastic.preservesProb_iff_exists_angles
import Mathlib
import Definitions.Def_ChapterEulerStochastic
open BookProof.ChapterEulerStochastic


open scoped Matrix BigOperators

Formal statement

theorem BookProof.ChapterEulerStochastic.preservesProb_iff_exists_angles (M : Matrix (Fin 2) (Fin 2) ℝ) :
    PreservesProb M ↔ ∃ a b : ℝ, M = Mmat a b := by sorry

View graph