def automorphism_of_fin_2 (f : Fin 2 → Fin 2) : Prop

Equations

• automorphism_of_fin_2 f = (Function.Bijective f ∧ ∀ (x y : Fin 2), f x + f y = f (x + y))

theorem fin2 (x : Fin 2) : x = 0 ∨ x = 1

theorem fin2_rigid (f : Fin 2 → Fin 2) (hf : automorphism_of_fin_2 f) : f = id

Fin 2 is rigid as an additive structure.

def automorphism_of_fin_k (k : ℕ) (f : Fin k → Fin k) : Prop

Equations

• automorphism_of_fin_k k f = (Function.Bijective f ∧ ∀ (x y : Fin k), f x + f y = f (x + y))

def is_rigid (k : ℕ) : Prop

Equations

• is_rigid k = ∀ (g : Fin k → Fin k), automorphism_of_fin_k k g → g = id