Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-19 09:24 4e861f25

View on Github →

feat(group_theory/submonoid/basic): weaken assumptions for has_one instance to one_mem_class for set_like subobjects (#16104)

Estimated changes

Modified src/algebra/algebra/subalgebra/basic.lean

Modified src/algebra/direct_sum/basic.lean

Modified src/algebra/direct_sum/decomposition.lean

Modified src/algebra/module/injective.lean

Modified src/field_theory/intermediate_field.lean

Modified src/group_theory/submonoid/operations.lean

added theorem one_mem_class.coe_eq_one

added theorem one_mem_class.coe_one

added theorem one_mem_class.one_def

deleted theorem submonoid_class.coe_eq_one

deleted theorem submonoid_class.coe_one

deleted theorem submonoid_class.one_def

Modified src/ring_theory/graded_algebra/basic.lean

Modified src/ring_theory/graded_algebra/homogeneous_ideal.lean

Modified src/ring_theory/polynomial/basic.lean