Commit 2025-02-10 17:54 ac7f4397

View on Github →

chore(Algebra/BigOperators/Ring): don't import Field (#21656) Split the file into the part talking about rings and the part talking about fields. See https://github.com/leanprover-community/mathlib3/pull/2152 and https://github.com/leanprover-community/mathlib4/pull/19630 for the new copyright header.

Estimated changes