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