Theorem Subalgebra.FG.map

Modification history

2025-01-21 01:06

Mathlib/RingTheory/Adjoin/FG.lean

chore: replace open scoped Classical with `open scoped Classical in` or `classical` (#20501) …

Modified Subalgebra.FG.map View on Github →

2023-05-16 06:36

Mathlib/RingTheory/Adjoin/FG.lean

refactor: rename `Fg` to `FG` (#3948) …

Added Subalgebra.FG.map View on Github →