lemma proved tactic proof

`floor_abs_intCast`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  58lemma floor_abs_intCast (z : Int) : Int.floor (|((z : ℝ))|) = |z| := by

Tactic-mode proof.

  59  have habs : |((z : ℝ))| = ((|z| : Int) : ℝ) := by
  60    simp
  61  rw [habs]
  62  simpa using (Int.floor_intCast (R := ℝ) (z := |z|))
  63

From the project-wide theorem graph. These declarations reference this one in their body.

coeffMag_foldPlusOneStep in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use