Commit 2023-03-07 22:58 eb83c3de

chore: don't inline DivInvMonoid default value for Div, for better instance transparency (#1897) See Zulip. This will make particular DivInvMonoids whose Div field is constructed using the default value (such as ℝ) behave the same way as generic ones, at the instance transparency level, fixing examples such as the following:

import Mathlib.Data.Real.Basic
variable [LinearOrderedField α]
/- `.reducible` transparency works correctly over `ℝ`. -/
example {a b : ℝ} : a / 2 ≤ b / 2 := by
  with_reducible (apply mul_le_mul) -- fails, as desired
/- `.instance` transparency works correctly over a generic field. -/
example {a b : α} : a / 2 ≤ b / 2 := by
  with_reducible_and_instances (apply mul_le_mul) -- fails, as desired
/- `.instance` transparency does not work correctly over `ℝ`. -/
example {a b : ℝ} : a / 2 ≤ b / 2 := by
  with_reducible_and_instances (apply mul_le_mul) -- succeeds, wanted it not to
  all_goals sorry