Commit 2025-01-21 04:10 f380e8d1

chore(ConjAct): don't import fields (#20718) ConjAct is imported in basic algebra files about groups, and therefore should not import MonoidWithZero. The latter is currently quite deeply embedded within the import graph, so we start by removing Field. The copyright headers come from https://github.com/leanprover-community/mathlib3/pull/8627 and https://github.com/leanprover-community/mathlib3/pull/13439.