Commit 2024-12-08 07:41 31530f31

View on Github →

chore(AdicCompletion): generalise algebra instance to separate rings (#19466) In the existing instance Algebra R (AdicCompletion I R), R appears three times: On the left, on the right, and in I : Ideal R. The left occurrence can be generalised to a ring S such that R is a S-algebra. Closes ImperialCollegeLondon/FLT/issues/230. From FLT

Estimated changes

Modified Mathlib/RingTheory/AdicCompletion/Algebra.lean

Modified Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

modified theorem AdicCompletion.ext

modified theorem AdicCompletion.val_add

added theorem AdicCompletion.val_add_apply

added theorem AdicCompletion.val_neg

added theorem AdicCompletion.val_neg_apply

modified theorem AdicCompletion.val_smul

added theorem AdicCompletion.val_smul_apply

modified theorem AdicCompletion.val_sub

added theorem AdicCompletion.val_sub_apply

modified theorem AdicCompletion.val_sum

added theorem AdicCompletion.val_sum_apply

modified theorem AdicCompletion.val_zero

added theorem AdicCompletion.val_zero_apply

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean