Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
fix(data/zmod/algebra): fix
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Dec 13, 2021
1 parent 9bf076a commit cb8f851
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/data/zmod/algebra.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ variables {n : ℕ} (m : ℕ) [char_p R m]
/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n` -/
def algebra' (h : m ∣ n) : algebra (zmod n) R :=
{ smul := λ a r, a * r,
to_has_opposite_scalar := { smul := λ a r, r * a.unop },
commutes' := λ a r, show (a * r : R) = r * a,
begin
rcases zmod.int_cast_surjective a with ⟨k, rfl⟩,
Expand All @@ -29,6 +30,7 @@ def algebra' (h : m ∣ n) : algebra (zmod n) R :=
exact commute.cast_int_left r k,
end,
smul_def' := λ a r, rfl,
op_smul_def' := λ r a, rfl,
.. zmod.cast_hom h R }

end
Expand Down

0 comments on commit cb8f851

Please sign in to comment.