Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-10-02 09:30
9e54ad01
View on Github →
feat(ring_theory/algebraic_independent): algebraic independence (
#9229
)
Estimated changes
Created
src/ring_theory/algebraic_independent.lean
added
theorem
alg_hom.algebraic_independent_iff
added
theorem
algebraic_independent.aeval_comp_repr
added
def
algebraic_independent.aeval_equiv
added
theorem
algebraic_independent.aeval_repr
added
theorem
algebraic_independent.algebra_map_injective
added
theorem
algebraic_independent.coe_range
added
theorem
algebraic_independent.comp
added
theorem
algebraic_independent.eq_zero_of_aeval_eq_zero
added
theorem
algebraic_independent.image
added
theorem
algebraic_independent.image_of_comp
added
theorem
algebraic_independent.is_transcendence_basis_iff
added
theorem
algebraic_independent.linear_independent
added
theorem
algebraic_independent.map'
added
theorem
algebraic_independent.map
added
theorem
algebraic_independent.mono
added
theorem
algebraic_independent.ne_zero
added
theorem
algebraic_independent.of_comp
added
def
algebraic_independent.repr
added
theorem
algebraic_independent.repr_ker
added
theorem
algebraic_independent.restrict_of_comp_subtype
added
theorem
algebraic_independent.restrict_scalars
added
theorem
algebraic_independent.to_subtype_range'
added
theorem
algebraic_independent.to_subtype_range
added
def
algebraic_independent
added
theorem
algebraic_independent_Union_of_directed
added
theorem
algebraic_independent_adjoin
added
theorem
algebraic_independent_bounded_of_finset_algebraic_independent_bounded
added
theorem
algebraic_independent_comp_subtype
added
theorem
algebraic_independent_empty
added
theorem
algebraic_independent_empty_iff
added
theorem
algebraic_independent_empty_type
added
theorem
algebraic_independent_empty_type_iff
added
theorem
algebraic_independent_equiv'
added
theorem
algebraic_independent_equiv
added
theorem
algebraic_independent_finset_map_embedding_subtype
added
theorem
algebraic_independent_iff
added
theorem
algebraic_independent_iff_injective_aeval
added
theorem
algebraic_independent_iff_ker_eq_bot
added
theorem
algebraic_independent_image
added
theorem
algebraic_independent_of_finite
added
theorem
algebraic_independent_of_subsingleton
added
theorem
algebraic_independent_sUnion_of_directed
added
theorem
algebraic_independent_subtype
added
theorem
algebraic_independent_subtype_range
added
theorem
exists_maximal_algebraic_independent
added
def
is_transcendence_basis