Commit 2025-03-01 19:47 4d4152a9

View on Github →

chore: make commands start at the start of a line (#22441) Just some whitespace changes: both to commands in the wrong column, and unnecessary indents in docstrings.

Estimated changes

added theorem AlgHom.coe_ideal_map
added theorem AlgHom.comap_ker
added theorem AlgHom.ker_coe
added def Algebra.idealMap
deleted theorem Ideal.AlgHom.comap_ker
deleted theorem Ideal.AlgHom.ker_coe
deleted theorem Ideal.Ideal.ker_le_comap
deleted theorem Ideal.Ideal.map_sInf
deleted theorem Ideal.RingHom.comap_ker
deleted def Ideal.RingHom.ker
deleted theorem Ideal.RingHom.ker_eq
deleted theorem Ideal.RingHom.ker_equiv
deleted theorem Ideal.RingHom.ker_isPrime
deleted theorem Ideal.RingHom.ker_ne_top
deleted theorem Ideal.RingHom.mem_ker
added theorem Ideal.ker_le_comap
added theorem Ideal.map_sInf
added theorem Module.mem_annihilator
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_equiv_comp
added theorem RingHom.ker_isPrime
added theorem RingHom.ker_ne_top
added theorem RingHom.mem_ker