Modify Indicator

Probability/Basic.lean

@@ -1,3 +1,5 @@
+--Please add to main pretty pretty please
+--Broke everything
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Rat.Defs
@@ -26,7 +28,7 @@ def indicator (cond : Bool) : ℚ := cond.rec 0 1
 abbrev 𝕀 : Bool → ℚ := indicator
 
 /-- Indicator is 0 or 1 -/
-theorem ind_zero_one (cond : τ → Bool) (ω : τ) : ( (𝕀∘cond) ω = 1)∨((𝕀∘cond) ω = 0) := by
+theorem ind_zero_on (cond : τ → Bool) : ( (𝕀∘cond) ω = 1)∨((𝕀∘cond) ω = 0) := by
     by_cases h : cond ω
     · left; simp only [Function.comp_apply, h, indicator]
     · right; simp only [Function.comp_apply, h, indicator]

blueprint/src/print.tex

@@ -9,6 +9,7 @@
 % (no ugly rectangles around links).
 % It is otherwise a very minimal preamble (you should probably at least
 % add cleveref and tikz-cd).
+% broke everything
 
 \documentclass[letterpaper]{article}