parentheses in ZMod.mul_inv_of_unit

Stream: new members

[Zhang Qinchuan]

I change the parentheses (a : ZMod n) in ZMod.mul_inv_of_unit to curly bracket {a : ZMod n} with nothing happened. Is there any special reason to use parenthese here?

import Mathlib

namespace ZMod

theorem mul_inv_of_unit' {n : ℕ} {a : ZMod n} (h : IsUnit a) : a * a⁻¹ = 1 := by
  rcases h with ⟨u, rfl⟩
  rw [inv_coe_unit, u.mul_inv]

end ZMod

theorem curly_bracket {n : ℕ} {a : ZMod n} (h : IsUnit a) : a * a⁻¹ = 1 :=
  ZMod.mul_inv_of_unit' h

theorem parentheses {n : ℕ} {a : ZMod n} (h : IsUnit a) : a * a⁻¹ = 1 :=
  ZMod.mul_inv_of_unit _ h

[Violeta Hernández]

We sometimes require arguments to be passed in even when they could, in theory, be inferred. This happens most often when the argument is something that might be quite complicated to build, as in e.g. docs#PartialOrder.lift.

[Violeta Hernández]

I think in this case it's just an oversight, though

[Violeta Hernández]

Feel free to open a PR

[Johan Commelin]

It depends on the size of the diff. If it is used in many places where h is going to be a new goal, but a is supplied, then you might be fighting a small uphill battle.
I don't know

[Zhang Qinchuan]

Violeta Hernández said:

We sometimes require arguments to be passed in even when they could, in theory, be inferred. This happens most often when the argument is something that might be quite complicated to build, as in e.g. docs#PartialOrder.lift.

I have seen scary @ and _ in mathlib. For example :

-- mathlib4/Mathlib/GroupTheory/Sylow.lean
-- fixedPointsMulLeftCosetsEquivQuotient
(fun a => (@mem_fixedPoints_mul_left_cosets_iff_mem_normalizer _ _ _ ‹_› _).symm)

So in my mind, it is free to use @ when someone wants to pass implicit arguments by hand.

[Violeta Hernández]

Sure, that's always an option. You can also use (x := _) syntax to pass any named variables automatically.

[Violeta Hernández]

This is considered somewhat of an antipattern though, and a signal that the argument should have been explicit to begin with