Structures · Algebra
Submodule.IsPrincipal
An R-submodule of M is principal if it is generated by one element.
- Defined in
- Mathlib.LinearAlgebra.Span.Defs
- Shape
- One type argument · adds principal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by43
- Submodule.IsPrincipal.generator
- Ideal.span_singleton_generator
- IsBezout.gcd
- Submodule.IsPrincipal.mem_iff_generator_dvd
- Submodule.IsPrincipal.span_singleton_generator
- Submodule.IsPrincipal.principal
- Submodule.IsPrincipal.generator_mem
- Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero
- IsBezout.span_gcd
- IsRelPrime.isCoprime
- Submodule.IsPrincipal.prime_generator_of_isPrime
- Ideal.isoBaseOfIsPrincipal
- Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes
- Submodule.IsPrincipal.mem_iff_eq_smul_generator
- FractionalIdeal.eq_spanSingleton_of_principal
- IsBezout.gcd_dvd_right
- IsBezout.gcd_dvd_left
- IsBezout.dvd_gcd
- FractionalIdeal.mul_generator_self_inv
- Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing
- eq_bot_of_generator_maximal_submoduleImage_eq_zero
- Ideal.exists_normalized_span_of_isPrincipal
- IsBezout.gcd_eq_sum
- Ideal.subtype_isoBaseOfIsPrincipal_eq_mul
- dvd_generator_iff
- Ideal.IsPrincipal.of_comap
- isRelPrime_iff_isCoprime
- generator_maximal_submoduleImage_dvd
- IsBezout.associated_gcd_gcd
- FractionalIdeal.invertible_of_principal
- Submodule.IsPrincipal.generator_submoduleImage_dvd_of_mem
- instIsPrincipalMapRingHom
- Ideal.isoBaseOfIsPrincipal_apply
- Ideal.prime_generator_of_prime
- FractionalIdeal.isPrincipal_inv
- Submodule.IsPrincipal.of_comap
- IsBezout.gcd.congr_simp
- Ideal.isoBaseOfIsPrincipal.congr_simp
- FractionalIdeal.invertible_iff_generator_nonzero
- Submodule.IsPrincipal.generator_map_dvd_of_mem
- Submodule.IsPrincipal.dvd_generator_span_iff
- Submodule.IsPrincipal.generator.congr_simp
- eq_bot_of_generator_maximal_map_eq_zero
Ancestors0
No ancestors.