Theorem Algebra.Generators.ker_eq_ker_aeval_val

Modification history

2025-01-04 18:31

Mathlib/RingTheory/Generators.lean

chore(RingTheory/Generators): make algebra instance a def (#14265) …

Modified Algebra.Generators.ker_eq_ker_aeval_val View on Github →

2024-07-01 08:43

Mathlib/RingTheory/Generators.lean

feat(RingTheory): presentations of algebras (#14271) …

Added Algebra.Generators.ker_eq_ker_aeval_val View on Github →