Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 22:42 0cbba1a4

View on Github →

feat(ring_theory/adjoin/basic): add adjoin_induction' and adjoin_adjoin_coe_preimage (#10427) From FLT-regular.

Estimated changes

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.closure_closure_coe_preimage

Modified src/group_theory/submonoid/operations.lean

added theorem submonoid.closure_closure_coe_preimage

Modified src/linear_algebra/basic.lean

added theorem submodule.span_induction'

added theorem submodule.span_span_coe_preimage

Modified src/ring_theory/adjoin/basic.lean

added theorem algebra.adjoin_adjoin_coe_preimage

added theorem algebra.adjoin_induction'