Commit 2024-09-23 15:47 2aa39ca4

View on Github →

feat: add map_i[I]nf for sub(semi)ring, subalgebra, subfield etc. (#15113) ... which require that the map in question is injective (this automatically holds for fields). Added for:

  • sub(semi)group, submonoid, and their additive counterpart
  • sub(semi)ring, (star)subalgebra, and their non-unital counterpart
  • subfield and intermediate fields. Also add (coe|mem)_iInf for subfield and (non-unital)subsemiring.

Estimated changes

added theorem Algebra.map_iInf
added theorem Algebra.map_inf
added theorem Subfield.coe_iInf
added theorem Subfield.map_iInf
added theorem Subfield.map_inf
added theorem Subfield.mem_iInf
added theorem Subgroup.map_iInf
added theorem Subgroup.map_inf
added theorem Submonoid.map_iInf
added theorem Submonoid.map_inf
added theorem Subsemigroup.map_iInf
added theorem Subsemigroup.map_inf
added theorem Subring.map_iInf
added theorem Subring.map_inf
added theorem Subsemiring.coe_iInf
added theorem Subsemiring.map_iInf
added theorem Subsemiring.map_inf
added theorem Subsemiring.mem_iInf
added theorem StarSubalgebra.map_inf