Happy new year!

Stream: general

[Adam Topaz]

import Mathlib

open Padic in
theorem HappyNewYear (p : ℕ) [Fact p.Prime] :
    Nat.card ((ZMod 7 × ZMod 7) ≃+ (ZMod 7 × ZMod 7)) +
    Nat.card ((Fin 3 ≃ Fin 3) ≃* (Fin 3 ≃ Fin 3)) +
    Nat.card (ℝ ≃+* ℝ) +
    Nat.card (ℚ_[p] ≃+* ℚ_[p]) =
    2024 :=
  sorry

[Adam Topaz]

(Sorry for the edits, it should be doable now :))

[Frederick Pu]

Adam Topaz said:

import Mathlib

open Padic in
theorem HappyNewYear (p : ℕ) [Fact p.Prime] :
    Nat.card ((ZMod 7 × ZMod 7) ≃+ (ZMod 7 × ZMod 7)) +
    Nat.card ((Fin 3 ≃ Fin 3) ≃* (Fin 3 ≃ Fin 3)) +
    Nat.card (ℝ ≃+* ℝ) +
    Nat.card (ℚ_[p] ≃+* ℚ_[p]) =
    2024 :=
  sorry

Sorry if this is a stupid question but how are you able to chain equivalence together like that. What does it mean?

[Mauricio Collares]

The code snippet sums cardinalities of different sets of equivalences/isomorphisms

Edit: having read Yaël's answer I now understand the question

[Yaël Dillies]

Fin 3 ≃ Fin 3 is a group, namely the symmetric group on three elements. In particular, we can talk about endomorphisms of it.

[Frederick Pu]

Yaël Dillies said:

Fin 3 ≃ Fin 3 is a group, namely the symmetric group on three elements. In particular, we can talk about endomorphisms of it.

Is there a coercion from equivalence to endomorphism to group?

[Junyan Xu]

It's just a Group isntance docs#Equiv.Perm.permGroup on Equiv.perm α which is defined to be α ≃ α reducibly.