Commit 2025-04-15 08:18 679ed8e6

chore: move and rename eval_of_algHom (#23952) Also generalize slightly and turn [Fintype] [DecidableEq] to [Finite]. I think the correct condition on k is that it's nontrivial and not a direct product of two nontrivial semirings, i.e. its PrimeSpectrum is connected. If this is violated, we get counterexamples like (R₁ × R₂) × (R₁ × R₂) → R₁ × R₂ given by (r₁₁, r₁₂), (r₂₁, r₂₂)) ↦ (r₁₁, r₂₂).