Structures · Algebra
RingHomSurjective
Class expressing the fact that a RingHom is surjective. This is needed in the context
of semilinear maps, where some lemmas require this.
- Defined in
- Mathlib.Algebra.Ring.CompTypeclasses
- Shape
- One type argument · adds is_surjective
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by217
- LinearMap.range
- Submodule.map
- LinearMap.range_eq_top
- Submodule.map_top
- Submodule.map_span
- Submodule.map.congr_simp
- LinearMap.range_comp
- Submodule.map_le_iff_le_comap
- LinearMap.rangeRestrict
- LinearMap.mem_range_self
- Submodule.map_injective_of_injective
- LinearMap.range_eq_map
- Submodule.FG.map
- Submodule.span_image
- Submodule.mem_map
- Submodule.comap_map_eq
- Submodule.map_bot
- Submodule.mem_map_of_mem
- Submodule.map_comp
- LinearMap.range.congr_simp
- Submodule.map_comap_eq
- Submodule.map_sup
- Submodule.orderIsoMapComap
- LinearMap.mem_range
- ContinuousLinearMap.precomp
- Submodule.map_mono
- LinearMap.submoduleMap
- Submodule.map_iSup
- LinearMap.range_eq_top_of_surjective
- LinearMap.coe_range
- LinearMap.range_codRestrict
- Submodule.gciMapComap
- Submodule.range_liftQ
- Submodule.giMapComap
- Submodule.map_coe
- LinearMap.range_zero
- LinearMap.map_span
- LinearMap.range_comp_le_range
- RingHom.surjective
- LinearMap.range_comp_of_range_eq_top
- LinearMap.range_le_ker_iff
- LinearMap.range_rangeRestrict
- Submodule.map_comap_eq_of_surjective
- Submodule.orderIsoMapComapOfBijective
- Submodule.comap_injective_of_surjective
- Submodule.map_le_map_iff_of_injective
- ContinuousLinearMap.rangeRestrict
- LinearMap.range_eq_bot
- LinearMap.map_le_range
- LinearMap.range_le_iff_comap
Ancestors0
No ancestors.