Theorems · Theorem · ring theory
RingHom.id_apply
∀ {α : Type u_2} {x : NonAssocSemiring α} (x_1 : α), (RingHom.id α) x_1 = x_1- Defined in
- Mathlib.Algebra.Ring.Hom.Defs
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- RingHom.idstatement · cited by 18,349
- RingHomstatement · cited by 10,189
- NonAssocSemiringstatement and proof · cited by 805
Cited by21
Results whose statement or proof uses this declaration.
- Polynomial.eval_smulproof · cited by 12
- RootPairing.InvariantForm.pairing_mul_eq_pairing_mul_swapproof · cited by 6
- PerfectRing.liftAux_id_applyproof · cited by 3
- Matrix.toLinearMap₂'_applyproof · cited by 3
- LinearMap.BilinForm.apply_sq_le_of_symmproof · cited by 2
- LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_selfproof · cited by 2
- MvPolynomial.transcendental_polynomial_aeval_Xproof · cited by 2
- separate_convex_open_setproof · cited by 2
- RootPairing.zero_lt_pairingIn_iffproof · cited by 2
- ContinuousLinearMap.exists_approx_preimage_norm_leproof · cited by 1
- RieszExtension.stepproof · cited by 1
- Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomialsproof · cited by 1