ite_div ?

Stream: mathlib4

[Michael Stoll]

There are docs#add_ite, docs#ite_add, docs#mul_ite, docs#ite_mul (docs#ite_neg is of a different flavor), but I'm missing for example

import Mathlib.Logic.Basic

lemma ite_div {α : Type*} [Div α] (P : Prop) [Decidable P] (a b c : α) :
    (if P then a else b) / c = if P then a / c else b / c := by
  refine eq_ite_iff.mpr ?_
  by_cases h : P
  · simp only [h, ite_true, and_self, not_true_eq_false, false_and, or_false]
  · simp only [h, ite_false, false_and, not_false_eq_true, and_self, or_true]

Is there a reason why thre are no analogous lemmas for div etc.?

[Junyan Xu]

Not sure why but

import Mathlib.Logic.Basic
lemma ite_div {α : Type*} [Div α] (P : Prop) [Decidable P] (a b c : α) :
    (if P then a else b) / c = if P then a / c else b / c :=
  apply_ite (· / c) P a b

[Michael Stoll]

A plain ite_div would be easier to use when the relevant expression involves bound variables, but combining conv with docs#apply_ite eventually worked out.

[Yury G. Kudryashov]

Since we have ite_mul and mul_ite, I think it's OK to add ite_div and div_ite. I would add these lemmas very early, maybe in Mathlib/Algebra/Group/Basic.

[Yury G. Kudryashov]

If you're going to PR this, then please move ite_mul and mul_ite to the same file and use apply_ite in all proofs. Also please add dite versions.

[Junyan Xu]

I feel we just need a ite_apply for functions with two arguments where the ite is in the first argument. (If it's in the last argument rewriting using docs#apply_ite should work without trouble.) There is apply_ite₂ but there both arguments are ite.

[Junyan Xu]

Maybe not even that ... by rw [apply_ite (· / c)] already works in this example. What could be other reason(s) that we want ite_div?

[Yaël Dillies]

Yeah, the thing is that every function has an ite lemma.