IMO 2012 A5 (𝔽₃Map2)

We define 𝔽₃Map2 : 𝔽₃ → ℤ and prove that it is a good map.

def IMOSL.IMO2012A5.Generalization.𝔽₃Map2 : 𝔽₃ → ℤ

Equations

• IMOSL.IMO2012A5.Generalization.𝔽₃Map2 IMOSL.IMO2012A5.Generalization.𝔽₃.𝔽₃0 = -1
• IMOSL.IMO2012A5.Generalization.𝔽₃Map2 IMOSL.IMO2012A5.Generalization.𝔽₃.𝔽₃1 = 0
• IMOSL.IMO2012A5.Generalization.𝔽₃Map2 IMOSL.IMO2012A5.Generalization.𝔽₃.𝔽₃2 = 0

theorem IMOSL.IMO2012A5.Generalization.𝔽₃Map2_is_good : good 𝔽₃Map2

The map 𝔽₃Map2 is good.

theorem IMOSL.IMO2012A5.Generalization.𝔽₃Map2_is_NontrivialGood : NontrivialGood 𝔽₃Map2

The map 𝔽₃Map2 is non-trivial good.