English
If hab is a domain for a / b, then the value of (a / b).get hab equals a.get (left_dom_of_div_dom hab) divided by b.get (right_dom_of_div_dom hab).
Русский
Если hab — домен для a / b, то значение (a / b).get hab равно a.get (left_dom_of_div_dom hab) делённому на b.get (right_dom_of_div_dom hab).
LaTeX
$$$ (a / b).get\ hab = a.get (left\_dom\_of\_div\_dom hab) / b.get (right\_dom\_of\_div\_dom hab) $$$
Lean4
@[to_additive (attr := simp)]
theorem div_get_eq [Div α] (a b : Part α) (hab : Dom (a / b)) :
(a / b).get hab = a.get (left_dom_of_div_dom hab) / b.get (right_dom_of_div_dom hab) := by simp [div_def]; aesop
