missing instance of infinitude of units of groupwithzero

Stream: new members

[Alex Brodbelt]

Assuming the code below is relevant to mathlib, where do I place this instance?

In view of docs#IsAlgClosed.instInfinite, I was thinking of placing it in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/GroupWithZero/Units/Basic.lean

but I think that would require some imports or other things where there might be conventions I am not aware of.

I need the specific case for fields in my project but this is the most general to my mind. I also recognise the formalization might be a bit roundabout stepping into Set world?

import Mathlib

instance {G : Type*} [GroupWithZero G] [hG : Infinite G] : Infinite Gˣ := by
  let units_equiv : (Set.univ : Set Gˣ) ≃ Units.val '' Set.univ :=
    Equiv.Set.image Units.val Set.univ (@Units.val_injective G _)
  have units_ne_zero : Units.val '' Set.univ = Set.univ \ {(0 : G)} := by
    ext x
    constructor
    · grind [Units.ne_zero]
    · intro hx
      exists Units.mk0 x (by simpa using hx.right)
  rw [← Set.infinite_univ_iff, ← Set.infinite_coe_iff,
        Equiv.infinite_iff (units_equiv), Set.infinite_coe_iff,
        units_ne_zero]
  exact Set.Infinite.diff (Set.infinite_univ_iff.mpr hG) (Set.finite_singleton 0)

[Eric Wieser]

This seems like a nicer aproach to me:

import Mathlib

@[simp]
theorem Option.finite_iff {α : Type*} : Finite (Option α) ↔ Finite α where
  mpr _ := instFiniteOption
  mp
  | @Finite.intro _ 0 e => (e none).elim0
  | @Finite.intro _ (n + 1) e => ⟨(e.trans (finSuccEquiv n)).removeNone⟩

@[simp]
theorem Subtype.finite_ne_iff {α : Type*} (a₀ : α) : Finite {a // a ≠ a₀} ↔ Finite α := by
  classical
  rw [← (Equiv.optionSubtypeNe a₀).finite_iff, Option.finite_iff]

@[simp]
theorem Units.finite_iff₀ {G : Type*} [GroupWithZero G] : Finite Gˣ ↔ Finite G := by
  rw [unitsEquivNeZero.finite_iff, Subtype.finite_ne_iff]

@[simp]
theorem Units.infinite_iff₀ {G : Type*} [GroupWithZero G] : Infinite Gˣ ↔ Infinite G := by
  simpa only [not_finite_iff_infinite] using Units.finite_iff₀ (G := G).not

instance {G : Type*} [GroupWithZero G] [hG : Infinite G] : Infinite Gˣ :=
  Units.infinite_iff₀.2 ‹_›

[Alex Brodbelt]

Ah yes wow, that is much nicer

[Eric Wieser]

Or a more fun way to do it:

def Option.fintypeEquiv : Fintype (Option α) ≃ Fintype α where
  invFun f := inferInstance
  toFun of := { elems := Finset.univ.eraseNone, complete a := by simp }
  left_inv f := Subsingleton.elim _ _
  right_inv f := Subsingleton.elim _ _

@[simp]
theorem Option.finite_iff {α : Type*} : Finite (Option α) ↔ Finite α := by
  simpa [← finite_iff_nonempty_fintype] using Option.fintypeEquiv (α := α).nonempty_congr

[Alex Brodbelt]

I see so you would add this last snippet to some file regarding Finite/Fintype and then add the instance for GroupWithZero calling this result?

[Alex Brodbelt]

(deleted)

[Eric Wieser]

Probably all the lemmas / instances above should go somewhere, and some time with #find_home might be able to track down where