Commit 2024-05-11 08:45 01f894dc

View on Github →

chore: split RingTheory.Ideal.Operations (#12777) Split the file RingTheory.Ideal.Operations into two parts by putting everything related to maps into a new file called... RingTheory.Ideal.Maps.

Estimated changes

added theorem AlgHom.coe_ideal_map
added theorem AlgHom.coe_ker
added theorem Ideal.IsRadical.comap
added theorem Ideal.coe_comap
added def Ideal.comap
added theorem Ideal.comap_comap
added theorem Ideal.comap_eq_top_iff
added theorem Ideal.comap_iInf
added theorem Ideal.comap_id
added theorem Ideal.comap_inf
added theorem Ideal.comap_isPrime
added theorem Ideal.comap_map_comap
added theorem Ideal.comap_mono
added theorem Ideal.comap_ne_top
added theorem Ideal.comap_of_equiv
added theorem Ideal.comap_radical
added theorem Ideal.comap_sInf'
added theorem Ideal.comap_sInf
added theorem Ideal.comap_symm
added theorem Ideal.comap_top
added theorem Ideal.gc_map_comap
added def Ideal.giMapComap
added theorem Ideal.ker_le_comap
added theorem Ideal.le_comap_map
added theorem Ideal.le_comap_mul
added theorem Ideal.le_comap_pow
added theorem Ideal.le_comap_sup
added theorem Ideal.map.isMaximal
added def Ideal.map
added def Ideal.mapHom
added theorem Ideal.map_bot
added theorem Ideal.map_comap_le
added theorem Ideal.map_comap_map
added theorem Ideal.map_iSup
added theorem Ideal.map_id
added theorem Ideal.map_inf_le
added theorem Ideal.map_map
added theorem Ideal.map_mono
added theorem Ideal.map_mul
added theorem Ideal.map_of_equiv
added theorem Ideal.map_radical_le
added theorem Ideal.map_sInf
added theorem Ideal.map_sSup
added theorem Ideal.map_span
added theorem Ideal.map_sup
added theorem Ideal.map_symm
added theorem Ideal.map_top
added theorem Ideal.mem_comap
added theorem Ideal.mem_map_of_mem
added theorem Ideal.smul_top_eq_map
added theorem Pi.ker_ringHom
added theorem RingHom.comap_ker
added def RingHom.ker
added theorem RingHom.ker_coe_equiv
added theorem RingHom.ker_eq
added theorem RingHom.ker_equiv
added theorem RingHom.ker_isPrime
added theorem RingHom.ker_ne_top
added theorem RingHom.mem_ker
deleted theorem AlgHom.coe_ideal_map
deleted theorem AlgHom.coe_ker
deleted theorem Ideal.IsRadical.comap
deleted theorem Ideal.apply_coe_mem_map
deleted theorem Ideal.coe_comap
deleted theorem Ideal.coe_restrictScalars
deleted def Ideal.comap
deleted theorem Ideal.comap_comap
deleted theorem Ideal.comap_eq_top_iff
deleted theorem Ideal.comap_iInf
deleted theorem Ideal.comap_id
deleted theorem Ideal.comap_inf
deleted theorem Ideal.comap_isPrime
deleted theorem Ideal.comap_le_iff_le_map
deleted theorem Ideal.comap_map_comap
deleted theorem Ideal.comap_mono
deleted theorem Ideal.comap_ne_top
deleted theorem Ideal.comap_of_equiv
deleted theorem Ideal.comap_radical
deleted theorem Ideal.comap_sInf'
deleted theorem Ideal.comap_sInf
deleted theorem Ideal.comap_symm
deleted theorem Ideal.comap_top
deleted theorem Ideal.gc_map_comap
deleted def Ideal.giMapComap
deleted theorem Ideal.ker_le_comap
deleted theorem Ideal.le_comap_map
deleted theorem Ideal.le_comap_mul
deleted theorem Ideal.le_comap_of_map_le
deleted theorem Ideal.le_comap_pow
deleted theorem Ideal.le_comap_sup
deleted theorem Ideal.map.isMaximal
deleted def Ideal.map
deleted def Ideal.mapHom
deleted theorem Ideal.map_bot
deleted theorem Ideal.map_comap_le
deleted theorem Ideal.map_comap_map
deleted theorem Ideal.map_comap_of_equiv
deleted theorem Ideal.map_iSup
deleted theorem Ideal.map_id
deleted theorem Ideal.map_inf_le
deleted theorem Ideal.map_le_iff_le_comap
deleted theorem Ideal.map_le_of_le_comap
deleted theorem Ideal.map_map
deleted theorem Ideal.map_mono
deleted theorem Ideal.map_mul
deleted theorem Ideal.map_of_equiv
deleted theorem Ideal.map_radical_le
deleted theorem Ideal.map_sInf
deleted theorem Ideal.map_sSup
deleted theorem Ideal.map_span
deleted theorem Ideal.map_sup
deleted theorem Ideal.map_symm
deleted theorem Ideal.map_top
deleted theorem Ideal.mem_comap
deleted theorem Ideal.mem_map_of_mem
deleted theorem Ideal.restrictScalars_mul
deleted theorem Ideal.smul_top_eq_map
deleted theorem Pi.ker_ringHom
deleted theorem RingHom.comap_ker
deleted def RingHom.ker
deleted theorem RingHom.ker_coe_equiv
deleted theorem RingHom.ker_eq
deleted theorem RingHom.ker_eq_comap_bot
deleted theorem RingHom.ker_equiv
deleted theorem RingHom.ker_isPrime
deleted theorem RingHom.ker_ne_top
deleted theorem RingHom.ker_rangeRestrict
deleted theorem RingHom.mem_ker
deleted theorem RingHom.not_one_mem_ker
deleted theorem RingHom.sub_mem_ker_iff