Theorem: Lean4Axiomatic.Integer.one_mul_one_eqv_one (Lean4Axiomatic/Integer/Sign.lean)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
⊢ 1 * 1 ≃ 1
Tactic:
exact AA.identL
State after:
no goals