Theorem: FinInt.mod2_zero (MLIR/Util/FinInt.lean)

State before:
n : ℕ
⊢ mod2 0 n = 0
Tactic:
simp [mod2]
State after:
n : ℕ
⊢ 2 ^ n % 2 ^ n = 0

State before:
n : ℕ
⊢ 2 ^ n % 2 ^ n = 0
Tactic:
simp [Int.emod_self]
State after:
no goals