Theorem Subring.closure_induction'

Modification history

2024-10-15 22:29

Mathlib/Algebra/Ring/Subring/Basic.lean

refactor: migrate to dependent induction lemmas (#17543) …

Deleted Subring.closure_induction'View on Github →

2023-09-12 09:41

Mathlib/RingTheory/Subring/Basic.lean

feat: maps from the unitization of non-unital subobjects of unital algebras (#6372) …

Added Subring.closure_induction'View on Github →

2023-08-22 22:24

Mathlib/RingTheory/Subring/Basic.lean

revert: #5602 (#6717) …

Deleted Subring.closure_induction'View on Github →

2023-08-04 08:48

Mathlib/RingTheory/Subring/Basic.lean

feat: maps between the unitization of a non-unital subalgebra and its `Algebra.adjoin` (#5602) …

Added Subring.closure_induction'View on Github →