## Stream: general

### Topic: What should set.has_inv do?

#### Eric Wieser (Feb 11 2022 at 21:53):

Given the following setup

import linear_algebra.matrix.nonsingular_inverse
import algebra.pointwise
open_locale pointwise cardinal


and knowing that:

example : #↥(({0} : set ℚ)⁻¹) = 1 := by simp [set.inv_singleton]


What would you expect right choice of _ to be here?

example : #↥(({0} : set (matrix (fin 2) (fin 2) ℚ))⁻¹) = _ := sorry


#### Eric Wieser (Feb 11 2022 at 21:54):

/poll What should the _ be?

• 0
• 1
• ω

#### Yaël Dillies (Feb 11 2022 at 21:56):

Having it be the preimage is nice, right? at least when it's involutive...

#### Adam Topaz (Feb 11 2022 at 22:08):

I think this operation should apply has_inv.inv to everything in the set.

#### Reid Barton (Feb 11 2022 at 22:08):

By default it should not exist unless someone has a use for it

Yeah, that too.

#### Adam Topaz (Feb 11 2022 at 22:12):

It's very common, e.g. in group theory, to write $S^{-1}$, $g \cdot S$, $S \cdot g$, $S \cdot S$, etc., where $S$ is a subset and g is an element of some group.

#### Reid Barton (Feb 11 2022 at 22:17):

Great, then give the instance a group constraint.

#### Adam Topaz (Feb 11 2022 at 22:18):

Can we make something like this work in Lean4?

variable (G : Type u) [Mul G]

instance (M : Type u → Type u) [Monad M] : Mul (M G) where
mul a b := return (← a) * (← b)

instance (M : Type u → Type u) [Monad M] : HMul G (M G) (M G) where
hMul a b := return a * (← b)

instance (M : Type u → Type u) [Monad M] : HMul (M G) G (M G) where
hMul a b := return (← a) * b


This typechecks, but it is a good idea?

#### Adam Topaz (Feb 11 2022 at 22:27):

Anyway, I think this is a perfectly reasonable instance:

import data.set.basic
instance {α : Type*} [has_inv α] : has_inv (set α) := ⟨λ S, (λ t : α, t⁻¹) '' S⟩


#### Yury G. Kudryashov (Feb 12 2022 at 00:01):

Reid Barton said:

By default it should not exist unless someone has a use for it

You need to open_locale pointwise to have this and other instances.

#### Adam Topaz (Feb 12 2022 at 01:02):

Oh, I didn't know that existed.

Last updated: Aug 03 2023 at 10:10 UTC