Commit 2023-10-30 19:25 2b448f2d

View on Github →

refactor(Algebra/Algebra/Subalgebra/Basic): use a better defeq for ⊥ : Subalgebra R A (#8038) And the same thing for StarSubalgebra R A. IntermediateField was already handled in #7957. As a result, nine (obvious) lemmas are now true by definition. This slightly adjusts the statement of Algebra.toSubmodule_bot to make it simpler and true by definition; the original statement can be recovered by rewriting by Submodule.one_eq_span, which I've had to add in some downstream proofs.

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

modified theorem Algebra.coe_bot

modified theorem Algebra.mem_bot

modified theorem Algebra.toSubmodule_bot

added theorem Subalgebra.toSubmodule_injective

Modified Mathlib/Algebra/Star/Subalgebra.lean

modified theorem StarSubalgebra.bot_toSubalgebra

modified theorem StarSubalgebra.coe_bot

modified theorem StarSubalgebra.mem_bot

Modified Mathlib/FieldTheory/Adjoin.lean

modified theorem IntermediateField.coe_bot

Modified Mathlib/LinearAlgebra/Finrank.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/IntegralClosure.lean

Modified Mathlib/Topology/Instances/Complex.lean