mathlib3

56511573 - feat(linear_algebra/adic_completion): le_jacobson_bot (#9125)

feat(linear_algebra/adic_completion): le_jacobson_bot (#9125) This PR proves that in an `I`-adically complete commutative ring `R`, the ideal `I` is contained in the Jacobson radical of `R`. Co-authored-by: Johan Commelin <johan@commelin.net>